Add coq.env.add-context for inserting a context declaration

builtin-doc/coq-builtin.elpi

@@ -817,6 +817,17 @@ coq.env.add-section-variable Name Ty C :-
   coq.env.add-section-variable-two Name explicit Ty C.
 
 
+
+pred coq.env.add-context i:context-decl.
+coq.env.add-context context-end.
+coq.env.add-context (context-item Name I Ty none Rest) :-
+  coq.env.add-section-variable-two Name I Ty C,
+  coq.env.add-context (Rest {coq.env.global (const C)}).
+coq.env.add-context (context-item Name _I Ty (some Bo) Rest) :-
+  coq.env.add-const Name Bo Ty ff C,
+  coq.env.add-context (Rest {coq.env.global (const C)}).
+
+
 % [coq.env.add-indt Decl I] Declares an inductive type.
 % Supported attributes:
 % - @dropunivs! (default: false, drops all universe constraints from the

src/coq_elpi_builtins.ml

@@ -2060,6 +2060,17 @@ coq.env.add-section-variable Name Ty C :-
   coq.env.add-section-variable-two Name explicit Ty C.
 |};
 
+  LPCode {|
+pred coq.env.add-context i:context-decl.
+coq.env.add-context context-end.
+coq.env.add-context (context-item Name I Ty none Rest) :-
+  coq.env.add-section-variable-two Name I Ty C,
+  coq.env.add-context (Rest {coq.env.global (const C)}).
+coq.env.add-context (context-item Name _I Ty (some Bo) Rest) :-
+  coq.env.add-const Name Bo Ty ff C,
+  coq.env.add-context (Rest {coq.env.global (const C)}).
+|};
+
   MLCode(Pred("coq.env.add-indt",
     CIn(indt_decl_in, "Decl",
     Out(inductive, "I",

tests/test_API_context.v

@@ -0,0 +1,19 @@
+From elpi Require Import elpi.
+
+Elpi Command context.
+Elpi Accumulate lp:{{
+  main [ctx-decl Ctx] :- !,
+    coq.env.add-context Ctx.
+}}.
+
+Section CA.
+  Elpi context Context (a : nat) [b : nat] {c : nat} (d : nat := 3) (e := 4).
+  Check eq_refl : d = 3.
+  Check eq_refl : e = 4.
+  Definition foo := a + b + c + d + e.
+End CA.
+Print foo.
+
+Elpi Query lp:{{
+  coq.arguments.implicit {coq.locate "foo"} [[explicit, implicit, maximal]].
+}}.