Add an implicitness argument to coq.env.add-section-variable

LPCIC · Jan 7, 2025 · 1458cc6 · 1458cc6
1 parent ee28024
commit 1458cc6
Show file tree

Hide file tree

Showing 5 changed files with 14 additions and 25 deletions.
diff --git a/builtin-doc/coq-builtin.elpi b/builtin-doc/coq-builtin.elpi
@@ -804,24 +804,18 @@ external pred coq.env.add-const i:id, i:term, i:term, i:opaque?,
 % - @inline-at! N (default: no inlining)
 external pred coq.env.add-axiom i:id, i:term, o:constant.
 
-% [coq.env.add-section-variable-two Name I Ty C] Declare a new section
-% variable: C gets a constant derived from Name
+% [coq.env.add-section-variable Name I Ty C] Declare a new section variable:
+% C gets a constant derived from Name
 % and the current module.
 % 
-external pred coq.env.add-section-variable-two i:id, i:implicit_kind, 
-                                               i:term, o:constant.
-
-
-pred coq.env.add-section-variable i:id, i:term, o:constant.
-coq.env.add-section-variable Name Ty C :-
-  coq.env.add-section-variable-two Name explicit Ty C.
-
+external pred coq.env.add-section-variable i:id, i:implicit_kind, i:term, 
+                                           o:constant.
 
 
 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-section-variable 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,

diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
@@ -2041,30 +2041,25 @@ Supported attributes:
      uctx, state, !: (global_constant_of_globref gr), []))),
   DocAbove);
 
-  MLCode(Pred("coq.env.add-section-variable-two",
+  MLCode(Pred("coq.env.add-section-variable",
     In(id,   "Name",
-    In(implicit_kind, "I",
+    In(B.unspec implicit_kind, "I",
     CIn(closed_ground_term, "Ty",
     Out(constant, "C",
     Full (global, {|Declare a new section variable: C gets a constant derived from Name
 and the current module.
 |}))))),
   (fun id bkind ty _ ~depth {options} _ -> grab_global_env_drop_sigma_keep_univs "coq.env.add-section-variable" (fun state ->
+     let bkind = Option.default Glob_term.Explicit (unspec2opt bkind) in
      let gr, uctx = add_axiom_or_variable "coq.env.add-section-variable" id ty (Some bkind) options state in
      uctx, state, !: (global_constant_of_globref gr), []))),
   DocAbove);
 
-  LPCode {|
-pred coq.env.add-section-variable i:id, i:term, o:constant.
-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-section-variable 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,

diff --git a/tests/test_API_section.v b/tests/test_API_section.v
@@ -17,8 +17,8 @@ Elpi Query lp:{{
   coq.locate "b" (const CB),
   coq.locate "c" (const CC),
   coq.env.const CC (some (global (const CB))) _,
-  coq.env.add-section-variable "d" {{ nat }} _,
-  coq.env.add-section-variable "d1" {{ nat }} _,
+  coq.env.add-section-variable "d" _ {{ nat }} _,
+  coq.env.add-section-variable "d1" _ {{ nat }} _,
   @local! => coq.env.add-const "e" {{ 3 }} {{ nat }} _ _.
 }}.
 About d.
@@ -33,7 +33,7 @@ Elpi Query lp:{{
   std.do! [ coq.env.begin-section "Foo", coq.env.end-section ]  
 }} lp:{{
   coq.env.begin-section "Foo",
-  coq.env.add-section-variable "x" {{ nat }} X,
+  coq.env.add-section-variable "x" _ {{ nat }} X,
   coq.env.section [X],
   coq.env.add-const "fx" (global (const X)) _ _ _,
   coq.env.end-section.

diff --git a/tests/test_HOAS.v b/tests/test_HOAS.v
@@ -62,7 +62,7 @@ Elpi Query lp:{{
   coq.env.begin-section "xxxxx",
   coq.univ.new U,
   T = sort (typ U),
-  coq.env.add-section-variable "a" T _,
+  coq.env.add-section-variable "a" _ T _,
   coq.env.end-section
 }}.
 

diff --git a/tests/test_glob.v b/tests/test_glob.v
@@ -19,7 +19,7 @@ Elpi Accumulate lp:{{
         field _ _ {{ @eq nat lp:f2 1 }} _\
         end-record)) _,
       coq.env.begin-section "A",
-      coq.env.add-section-variable "v" {{ nat }} _,
+      coq.env.add-section-variable "v" _ {{ nat }} _,
       coq.env.end-section,
       coq.env.begin-module "N2" none,
       coq.env.end-module _,