fix univ handling in coq.env.add-section-variable

LPCIC · Feb 11, 2021 · 599fb8a · 599fb8a
1 parent c0ede97
commit 599fb8a
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 2 deletions.
diff --git a/Changelog.md b/Changelog.md
@@ -4,6 +4,10 @@
 
 Requires Elpi 1.13 and Coq 8.13.
 
+### API
+- Fix `coq.env.add-section-variable` and `coq.env.add-axiom` were not handling
+  universes correctly.
+
 ### Build system
 
 - New target `build` which only builds elpi and the apps

diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
@@ -1219,7 +1219,7 @@ Supported attributes:
     Out(constant, "C",
     Full (global, {|Declare a new axiom: C gets a constant derived from Name
 and the current module|})))),
-  (fun id ty _ ~depth _ _ -> on_global_state_does_rewind_env "coq.env.add-axiom" (fun state ->
+  (fun id ty _ ~depth _ _ -> on_global_state "coq.env.add-axiom" (fun state ->
      let sigma = get_sigma state in
      let gr = add_axiom_or_variable "coq.env.add-axiom" id sigma ty false in
      state, !: (global_constant_of_globref gr), []))),
@@ -1231,7 +1231,7 @@ and the current module|})))),
     Out(constant, "C",
     Full (global, {|Declare a new section variable: C gets a constant derived from Name
 and the current module|})))),
-  (fun id ty _ ~depth _ _ -> on_global_state_does_rewind_env "coq.env.add-section-variable" (fun state ->
+  (fun id ty _ ~depth _ _ -> on_global_state "coq.env.add-section-variable" (fun state ->
      let sigma = get_sigma state in
      let gr = add_axiom_or_variable "coq.env.add-section-variable" id sigma ty true in
      state, !: (global_constant_of_globref gr), []))),