repair brain damage

src/coq_elpi_HOAS.ml

@@ -2283,7 +2283,17 @@ let grab_global_env_drop_sigma state =
     state
   end
 
-
+let grab_global_env_drop_sigma_keep_univs ~uctx state =
+  let env0 = get_global_env state in
+  let env = Global.env () in
+  if env == env0 then state
+  else begin
+    let sigma = get_sigma state in
+    let state = S.set engine state (CoqEngine_HOAS.from_env_keep_univ_of_sigma ~uctx ~env0 ~env sigma) in
+    let state = UVMap.empty state in
+    state
+  end
+
 let solvec = E.Constants.declare_global_symbol "solve"
 let msolvec = E.Constants.declare_global_symbol "msolve"
 let goalc = E.Constants.declare_global_symbol "goal"

src/coq_elpi_HOAS.mli

@@ -299,6 +299,7 @@ val body_of_constant :
 val grab_global_env : uctx:Univ.ContextSet.t -> State.t -> State.t
 val grab_global_env_drop_univs_and_sigma : State.t -> State.t
 val grab_global_env_drop_sigma : State.t -> State.t
+val grab_global_env_drop_sigma_keep_univs : uctx:Univ.ContextSet.t -> State.t -> State.t
 
 val mk_decl : depth:int -> Name.t -> ty:term -> term
 (* Adds an Arg for the normal form with ctx_len context entry vars in scope *)

src/coq_elpi_builtins.ml

@@ -141,7 +141,12 @@ let grab_global_env_drop_sigma api thunk = (); (fun state ->
   let state, result, gls = thunk state in
   Coq_elpi_HOAS.grab_global_env_drop_sigma state, result, gls)
 
-
+let grab_global_env_drop_sigma_keep_univs api thunk = (); (fun state ->
+  if State.get tactic_mode state then
+    Coq_elpi_utils.err Pp.(strbrk ("API " ^ api ^ " cannot be used in tactics"));
+  let uctx, state, result, gls = thunk state in
+  Coq_elpi_HOAS.grab_global_env_drop_sigma_keep_univs ~uctx state, result, gls)
+
 let bool = B.bool
 let int = B.int
 let list = B.list
@@ -2073,9 +2078,9 @@ Supported attributes:
     Full (global, {|Declare a new section variable: C gets a constant derived from Name
 and the current module.
 |})))),
-  (fun id ty _ ~depth {options} _ -> grab_global_env_drop_sigma "coq.env.add-section-variable" (fun state ->
-     let gr, _ = add_axiom_or_variable "coq.env.add-section-variable" id ty true options state in
-     state, !: (global_constant_of_globref gr), []))),
+  (fun id ty _ ~depth {options} _ -> grab_global_env_drop_sigma_keep_univs "coq.env.add-section-variable" (fun state ->
+     let gr, uctx = add_axiom_or_variable "coq.env.add-section-variable" id ty true options state in
+     uctx, state, !: (global_constant_of_globref gr), []))),
   DocAbove);
 
   MLCode(Pred("coq.env.add-indt",