From 19f99cf971ac2d556ffd8c4e297a2cde89c93fce Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 1 Mar 2023 15:48:37 +0100
Subject: [PATCH 1/8] test

---
 _CoqProject.test   |  1 +
 tests/test_ltac3.v | 23 +++++++++++++++++++++++
 2 files changed, 24 insertions(+)
 create mode 100644 tests/test_ltac3.v

diff --git a/_CoqProject.test b/_CoqProject.test
index e1f2f468e..6249ef934 100644
--- a/_CoqProject.test
+++ b/_CoqProject.test
@@ -27,6 +27,7 @@ tests/test_tactic.v
 tests/test_elaborator.v
 tests/test_ltac.v
 tests/test_ltac2.v
+tests/test_ltac3.v
 tests/test_cache_async.v
 tests/test_COQ_ELPI_ATTRIBUTES.v
 tests/perf_calls.v
diff --git a/tests/test_ltac3.v b/tests/test_ltac3.v
new file mode 100644
index 000000000..2201d5afe
--- /dev/null
+++ b/tests/test_ltac3.v
@@ -0,0 +1,23 @@
+From elpi Require Export elpi.
+From Coq Require Import ssreflect ssrfun ssrbool.
+
+Ltac ltac_foo := idtac.
+
+Record fooType := Foo { sort :> Type; }.
+Canonical unit_fooType := Foo unit.
+
+Elpi Tactic fail_foo.
+Elpi Accumulate lp:{{
+
+pred solve i:goal, o:list sealed-goal.
+solve (goal _ _ _ _ [_] as G) GS :-
+  coq.ltac.call "ltac_foo" [] G GS.
+
+}}.
+Elpi Typecheck.
+
+Goal True.
+Proof.
+elpi fail_foo ([the fooType of unit : Type]).
+exact I.
+Qed.

From b3c9d7bf0bab14e9316622ff865548a4346a84c4 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Thu, 2 Mar 2023 17:37:35 +0100
Subject: [PATCH 2/8] remove useless state component

---
 src/coq_elpi_HOAS.ml  | 12 ------------
 src/coq_elpi_HOAS.mli |  1 -
 2 files changed, 13 deletions(-)

diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml
index 79d853dc2..589b7c903 100644
--- a/src/coq_elpi_HOAS.ml
+++ b/src/coq_elpi_HOAS.ml
@@ -752,12 +752,6 @@ let in_elpi_primitive ~depth state i =
 
 (* {{{ HOAS : Evd.evar_map -> elpi *************************************** *)
 
-let command_mode =
-  S.declare ~name:"coq-elpi:command-mode"
-    ~init:(fun () -> true)
-    ~start:(fun x -> x)
-    ~pp:(fun fmt b -> Format.fprintf fmt "%b" b)
-
 module CoqEngine_HOAS : sig 
 
   val show_coq_engine : ?with_univs:bool -> coq_engine -> string
@@ -2112,8 +2106,6 @@ let sealed_goal2lp ~depth ~args ~in_elpi_tac_arg state k =
 
 let solvegoal2query sigma goals loc args ~in_elpi_tac_arg ~depth:calldepth state =
 
-  let state = S.set command_mode state false in (* tactic mode *)
-
   let state = S.set engine state (from_env_sigma (get_global_env state) sigma) in
 
   let state, gl, gls =
@@ -2147,7 +2139,6 @@ let customtac2query sigma goals loc text ~depth:calldepth state =
     let env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env in
     if not (Evd.is_undefined sigma goal) then
       err Pp.(str (Printf.sprintf "Evar %d is not a goal" (Evar.repr goal)));
-    let state = S.set command_mode state false in (* tactic mode *)
     let state = S.set engine state (from_env_sigma env sigma) in
     let state, elpi_goal_evar, elpi_raw_goal_evar, evar_decls = in_elpi_evar ~calldepth goal  state in
     let evar_concl, goal_ctx, goal_env =
@@ -3418,7 +3409,4 @@ let in_elpi_module_type (x : Declarations.module_type_body) = in_elpi_modty x
 
 (* ********************************* }}} ********************************** *)
 
-let command_mode = S.get command_mode
-
-
 (* vim:set foldmethod=marker: *)
diff --git a/src/coq_elpi_HOAS.mli b/src/coq_elpi_HOAS.mli
index e9350aaf0..dcc5a9b16 100644
--- a/src/coq_elpi_HOAS.mli
+++ b/src/coq_elpi_HOAS.mli
@@ -255,7 +255,6 @@ val body_of_constant :
   State.t -> Names.Constant.t -> Univ.Instance.t option ->
   State.t * EConstr.t option * Univ.Instance.t option
 
-val command_mode : State.t -> bool
 val grab_global_env : State.t -> State.t
 val grab_global_env_drop_univs : State.t -> State.t
 

From e51431a767cec97b36dc96a835be692efd07fbad Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Thu, 2 Mar 2023 17:38:22 +0100
Subject: [PATCH 3/8] remove useless assert false

---
 src/coq_elpi_glob_quotation.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml
index de0256fbf..d173207f4 100644
--- a/src/coq_elpi_glob_quotation.ml
+++ b/src/coq_elpi_glob_quotation.ml
@@ -28,7 +28,7 @@ let get_ctx, set_ctx, _update_ctx =
   let bound_vars =
     S.declare ~name:"coq-elpi:glob-quotation-bound-vars"
       ~init:(fun () -> None)
-      ~pp:(fun fmt -> function Some (x,_) -> () | None -> assert false)
+      ~pp:(fun fmt -> function Some (x,_) -> () | None -> ())
       ~start:(fun x -> x)
        in
   S.(get bound_vars, set bound_vars, update bound_vars)

From b527f22e43f7952a114843d5d09694f967a3b52a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Thu, 2 Mar 2023 17:44:59 +0100
Subject: [PATCH 4/8] quotations: use a dedicated environment

---
 src/coq_elpi_HOAS.ml           |  8 --------
 src/coq_elpi_HOAS.mli          |  5 -----
 src/coq_elpi_glob_quotation.ml | 21 +++++++++++++++++----
 3 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml
index 589b7c903..f669b9af5 100644
--- a/src/coq_elpi_HOAS.ml
+++ b/src/coq_elpi_HOAS.ml
@@ -2037,14 +2037,6 @@ let lp2constr syntactic_constraints coq_ctx ~depth state t =
 
 (* ********************************* }}} ********************************** *)
 
-let push_env state name =
-  let open Context.Rel.Declaration in
-  S.update engine state (fun ({ global_env } as x) ->
-     { x with global_env = Environ.push_rel (LocalAssum(Context.make_annot name Sorts.Relevant,C.mkProp)) global_env })
-let pop_env state =
-  S.update engine state (fun ({ global_env } as x) ->
-     { x with global_env = Environ.pop_rel_context 1 global_env })
-
 let set_sigma state sigma = S.update engine state (fun x -> { x with sigma })
 
 (* We reset the evar map since it depends on the env in which it was created *)
diff --git a/src/coq_elpi_HOAS.mli b/src/coq_elpi_HOAS.mli
index dcc5a9b16..bdf1d52f2 100644
--- a/src/coq_elpi_HOAS.mli
+++ b/src/coq_elpi_HOAS.mli
@@ -264,11 +264,6 @@ val mk_decl : depth:int -> Name.t -> ty:term -> term
 val mk_def :
   depth:int -> Name.t -> bo:term -> ty:term -> term
 
-(* Push a name with a dummy type (just for globalization to work) and
- * pop it back *)
-val push_env : State.t -> Names.Name.t -> State.t
-val pop_env : State.t -> State.t
-
 val get_global_env : State.t -> Environ.env
 val get_sigma : State.t -> Evd.evar_map
 val update_sigma : State.t -> (Evd.evar_map -> Evd.evar_map) -> State.t
diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml
index d173207f4..08f522a00 100644
--- a/src/coq_elpi_glob_quotation.ml
+++ b/src/coq_elpi_glob_quotation.ml
@@ -58,6 +58,19 @@ let is_restricted_name =
   let rex = Str.regexp "_elpi_restricted_[0-9]+_" in
   fun s -> Str.(string_match rex (Id.to_string s) 0)
 
+
+let glob_environment : Environ.env S.component =
+  S.declare ~name:"coq-elpi:glob-environment"
+    ~pp:(fun _ _ -> ()) ~init:Global.env ~start:(fun _ -> Global.env ())
+
+let push_env state name =
+  let open Context.Rel.Declaration in
+  S.update glob_environment state (Environ.push_rel (LocalAssum(Context.make_annot name Sorts.Relevant,Constr.mkProp)))
+let pop_env state =
+  S.update glob_environment state (Environ.pop_rel_context 1)
+  
+let get_glob_env state = S.get glob_environment state
+
 (* XXX: I don't get why we use a coq_ctx here *)
 let under_ctx name ty bo gterm2lp ~depth state x =
   let coq_ctx, hyps as orig_ctx = Option.default (upcast @@ mk_coq_context ~options:(default_options ()) state,[]) (get_ctx state) in
@@ -129,7 +142,7 @@ let noglsk f ~depth state = let state, x = f ~depth state in state, x, ()
 let rec gterm2lp ~depth state x =
   debug Pp.(fun () ->
       str"gterm2lp: depth=" ++ int depth ++
-      str " term=" ++Printer.pr_glob_constr_env (get_global_env state) (get_sigma state) x);
+      str " term=" ++Printer.pr_glob_constr_env (get_glob_env state) (get_sigma state) x);
   match (DAst.get x) (*.CAst.v*) with
   | GRef(GlobRef.ConstRef p,_ul) when Structures.PrimitiveProjections.mem p ->
       let p = Option.get @@ Structures.PrimitiveProjections.find_opt p in
@@ -160,7 +173,7 @@ let rec gterm2lp ~depth state x =
       let state, s = API.RawQuery.mk_Arg state ~name:(Printf.sprintf "type_%d" !type_gen) ~args:[] in
       state, in_elpi_flex_sort s
   | GSort(UNamed u) ->
-      let env = get_global_env state in
+      let env = get_glob_env state in
       in_elpi_sort ~depth state (sort_name env (get_sigma state) u)
   | GSort(_) -> nYI "(glob)HOAS for Type@{i j}"
 
@@ -270,7 +283,7 @@ let rec gterm2lp ~depth state x =
 
   | GCases(_, oty, [ t, (as_name, oind) ], bs) ->
       let open Declarations in
-      let env = get_global_env state in
+      let env = get_glob_env state in
       let ind, args_name =
         match oind with
         | Some {CAst.v=ind, arg_names} -> ind, arg_names
@@ -378,7 +391,7 @@ let coq_quotation ~depth state loc src =
   in
   let glob =
     try
-      Constrintern.intern_constr (get_global_env state) (get_sigma state) ce
+      Constrintern.intern_constr (get_glob_env state) (get_sigma state) ce
     with e ->
       CErrors.user_err
         Pp.(str(API.Ast.Loc.show loc) ++str":" ++ spc() ++ CErrors.print_no_report e)

From cbf7ff6e3989811d59288aa8a3944e1eb4e0216e Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Thu, 2 Mar 2023 17:46:15 +0100
Subject: [PATCH 5/8] harder test using abstract

---
 tests/test_ltac3.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/test_ltac3.v b/tests/test_ltac3.v
index 2201d5afe..73ea40577 100644
--- a/tests/test_ltac3.v
+++ b/tests/test_ltac3.v
@@ -1,7 +1,7 @@
 From elpi Require Export elpi.
 From Coq Require Import ssreflect ssrfun ssrbool.
 
-Ltac ltac_foo := idtac.
+Ltac ltac_foo := cut True; [ abstract trivial | idtac].
 
 Record fooType := Foo { sort :> Type; }.
 Canonical unit_fooType := Foo unit.

From c2631284a204bc2391c7bedd8340ff0f29be6777 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Fri, 3 Mar 2023 16:47:18 +0100
Subject: [PATCH 6/8] clarify env rewindin

---
 src/coq_elpi_HOAS.ml     | 49 +++++++++++++++++++++++++++++-----------
 src/coq_elpi_HOAS.mli    |  3 ++-
 src/coq_elpi_builtins.ml |  9 ++++----
 tests/test_ltac3.v       |  7 +++---
 4 files changed, 46 insertions(+), 22 deletions(-)

diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml
index f669b9af5..2ac24f6a2 100644
--- a/src/coq_elpi_HOAS.ml
+++ b/src/coq_elpi_HOAS.ml
@@ -758,9 +758,13 @@ module CoqEngine_HOAS : sig
 
   val engine : coq_engine S.component
 
-  val from_env_keep_univ_of_sigma : Environ.env -> Evd.evar_map -> coq_engine
   val from_env_sigma : Environ.env -> Evd.evar_map -> coq_engine
 
+  (* when the env changes under the hood, we can adapt sigma or drop it but keep
+     its constraints *)
+  val from_env_keep_univ_of_sigma : env0:Environ.env -> env:Environ.env -> Evd.evar_map -> coq_engine
+  val from_env_keep_univ_and_sigma : env0:Environ.env -> env:Environ.env -> Evd.evar_map -> coq_engine
+
 end = struct
 
  let pp_coq_engine ?with_univs fmt { sigma } =
@@ -776,10 +780,18 @@ let show_coq_engine ?with_univs e = Format.asprintf "%a" (pp_coq_engine ?with_un
 
  let from_env env = from_env_sigma env (Evd.from_env env)
 
- let from_env_keep_univ_of_sigma env sigma0 =
+ let from_env_keep_univ_and_sigma ~env0 ~env sigma0 =
+   assert(env0 != env);
+   let uctx = UState.update_sigma_univs (Evd.evar_universe_context sigma0) (Environ.universes env) in
+   let uctx = UState.demote_global_univs env uctx in
+   from_env_sigma env (Evd.set_universe_context sigma0 uctx)
+
+let from_env_keep_univ_of_sigma ~env0 ~env sigma0 =
+   assert(env0 != env);
    let uctx = UState.update_sigma_univs (Evd.evar_universe_context sigma0) (Environ.universes env) in
-   let sigma = Evd.from_ctx (UState.demote_global_univs env uctx) in
-   from_env_sigma env sigma
+  let uctx = UState.demote_global_univs env uctx in
+  from_env_sigma env (Evd.from_ctx uctx)
+ 
  let init () = from_env (Global.env ())
 
  let engine : coq_engine S.component =
@@ -1986,11 +1998,13 @@ and create_evar_unknown ~calldepth syntactic_constraints (coq_ctx : 'a coq_conte
 
   let state, (k, kty) = S.update_return engine state (fun ({ sigma } as e) ->
     let sigma, (ty, _) = Evarutil.new_type_evar ~naming:(Namegen.IntroFresh (Names.Id.of_string "e")) env sigma Evd.univ_rigid in
+    let ty_key, _ = EConstr.destEvar sigma ty in
     if on_ty then
-      { e with sigma }, (fst (EConstr.destEvar sigma ty), None)
+      { e with sigma }, (ty_key, None)
     else
       let sigma, t = Evarutil.new_evar ~typeclass_candidate:false ~naming:(Namegen.IntroFresh (Names.Id.of_string "e")) env sigma ty in
-      { e with sigma }, (fst (EConstr.destEvar sigma t), Some (fst (EConstr.destEvar sigma ty)))) in
+      let t_key, _ = EConstr.destEvar sigma t in
+      { e with sigma }, (t_key, Some ty_key)) in
   (*let state = S.update UVMap.uvmap state (UVMap.add elpi_evk k) in*)
   let state, gls_kty =
     match kty with
@@ -2046,22 +2060,31 @@ let grab_global_env state =
   if env == env0 then state
   else
     if Environ.universes env0 == Environ.universes env then
-      let state = S.set engine state (CoqEngine_HOAS.from_env_sigma env (Evd.from_ctx (Evd.evar_universe_context (get_sigma state)))) in
-      let state = UVMap.empty state in
+      let state = S.set engine state (CoqEngine_HOAS.from_env_sigma env (get_sigma state)) in
+      (*let state = UVMap.empty state in*)
       state  
     else
-      let state = S.set engine state (CoqEngine_HOAS.from_env_keep_univ_of_sigma env (get_sigma state)) in
-      let state = UVMap.empty state in
+      let state = S.set engine state (CoqEngine_HOAS.from_env_keep_univ_and_sigma ~env0 ~env (get_sigma state)) in
+      (*let state = UVMap.empty state in*)
       state
-let grab_global_env_drop_univs state =
+let grab_global_env_drop_univs_and_sigma state =
+  let env0 = get_global_env state in
   let env = Global.env () in
-  if env == get_global_env state then state
+  if env == env0 then state
   else
     let state = S.set engine state (CoqEngine_HOAS.from_env_sigma env (Evd.from_env env)) in
     let state = UVMap.empty state in
     state
 
-
+let grab_global_env_drop_sigma state =
+  let env0 = get_global_env state in
+  let env = Global.env () in
+  if env == env0 then state
+  else
+    let state = S.set engine state (CoqEngine_HOAS.from_env_keep_univ_of_sigma ~env0 ~env (get_sigma state)) in
+    let state = UVMap.empty state in
+    state
+    
 
 let solvec = E.Constants.declare_global_symbol "solve"
 let msolvec = E.Constants.declare_global_symbol "msolve"
diff --git a/src/coq_elpi_HOAS.mli b/src/coq_elpi_HOAS.mli
index bdf1d52f2..7aee54b44 100644
--- a/src/coq_elpi_HOAS.mli
+++ b/src/coq_elpi_HOAS.mli
@@ -256,7 +256,8 @@ val body_of_constant :
   State.t * EConstr.t option * Univ.Instance.t option
 
 val grab_global_env : State.t -> State.t
-val grab_global_env_drop_univs : 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 mk_decl : depth:int -> Name.t -> ty:term -> term
 (* Adds an Arg for the normal form with ctx_len context entry vars in scope *)
diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index 7fdc4d4f2..c7f643175 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -114,7 +114,7 @@ let on_global_state ?(abstract_exception=false) ?options api thunk = (); (fun st
     Coq_elpi_utils.err Pp.(strbrk ("API " ^ api ^ " cannot be used in tactics"));
   let state, result, gls = thunk state in
   match options with
-  | Some { keepunivs = Some false } -> Coq_elpi_HOAS.grab_global_env_drop_univs state, result, gls
+  | Some { keepunivs = Some false } -> Coq_elpi_HOAS.grab_global_env_drop_univs_and_sigma state, result, gls
   | _ -> Coq_elpi_HOAS.grab_global_env state, result, gls)
 
 (* This is for stuff that is not monotonic in the env, eg section closing *)
@@ -122,7 +122,7 @@ let on_global_state_does_rewind_env 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 state, result, gls = thunk state in
-  Coq_elpi_HOAS.grab_global_env_drop_univs state, result, gls)
+  Coq_elpi_HOAS.grab_global_env_drop_sigma state, result, gls)
 
 let warn_if_contains_univ_levels ~depth t =
   let global_univs = UGraph.domain (Environ.universes (Global.env ())) in
@@ -1988,7 +1988,7 @@ coq.env.begin-module Name MP :-
   MLCode(Pred("coq.env.end-module",
     Out(modpath, "ModPath",
     Full(unit_ctx, "end the current module that becomes known as ModPath *E*")),
-  (fun _ ~depth _ _ -> on_global_state "coq.env.end-module" (fun state ->
+  (fun _ ~depth _ _ -> on_global_state_does_rewind_env "coq.env.end-module" (fun state ->
      let mp = Declaremods.end_module () in
      state, !: mp, []))),
   DocAbove);
@@ -2023,7 +2023,7 @@ coq.env.begin-module-type Name :-
   MLCode(Pred("coq.env.end-module-type",
     Out(modtypath, "ModTyPath",
     Full(unit_ctx, "end the current module type that becomes known as ModPath *E*")),
-  (fun _ ~depth _ _ -> on_global_state "coq.env.end-module-type" (fun state ->
+  (fun _ ~depth _ _ -> on_global_state_does_rewind_env "coq.env.end-module-type" (fun state ->
      let mp = Declaremods.end_modtype () in
      state, !: mp, []))),
   DocAbove);
@@ -3476,7 +3476,6 @@ fold_left over the terms, letin body comes before the type).
            proofview pv in
 
        Declare.Internal.export_side_effects (Evd.eval_side_effects sigma);
-       let sigma = Evd.drop_side_effects sigma in
        
        let state, assignments = set_current_sigma ~depth state sigma in
        state, !: subgoals, assignments
diff --git a/tests/test_ltac3.v b/tests/test_ltac3.v
index 73ea40577..c925d2596 100644
--- a/tests/test_ltac3.v
+++ b/tests/test_ltac3.v
@@ -1,7 +1,8 @@
+
 From elpi Require Export elpi.
 From Coq Require Import ssreflect ssrfun ssrbool.
 
-Ltac ltac_foo := cut True; [ abstract trivial | idtac].
+Ltac ltac_foo := cut True; [ idtac | abstract (exact I) ].
 
 Record fooType := Foo { sort :> Type; }.
 Canonical unit_fooType := Foo unit.
@@ -16,8 +17,8 @@ solve (goal _ _ _ _ [_] as G) GS :-
 }}.
 Elpi Typecheck.
 
-Goal True.
+Goal nat.
 Proof.
 elpi fail_foo ([the fooType of unit : Type]).
-exact I.
+exact (fun _ => 0).
 Qed.

From d03554997bed1179d438ef899b54a18148a4a41c Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Sat, 4 Mar 2023 18:13:38 +0100
Subject: [PATCH 7/8] API: int/float->uint63/float64

---
 Changelog.md             |  5 +++++
 coq-builtin.elpi         |  8 ++++++++
 src/coq_elpi_builtins.ml | 16 ++++++++++++++++
 tests/test_API2.v        | 12 ++++++++++++
 4 files changed, 41 insertions(+)

diff --git a/Changelog.md b/Changelog.md
index 75e850a8e..d6edda36e 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,5 +1,10 @@
 # Changelog
 
+## UNRELEASED
+
+### API:
+- New `coq.int->uint63` and `coq.float->float64`
+
 ## [1.17.0] - 13/02/2023
 
 Requires Elpi 1.16.5 and Coq 8.17.
diff --git a/coq-builtin.elpi b/coq-builtin.elpi
index 5fee40732..a3ec9f224 100644
--- a/coq-builtin.elpi
+++ b/coq-builtin.elpi
@@ -1066,10 +1066,18 @@ type proj projection -> int -> primitive-value. % primitive projection
 % elpi integer I. Fails if it does not fit.
 external pred coq.uint63->int i:uint63, o:int.
 
+% [coq.int->uint63 I U] Transforms an elpi integer I into a primitive
+% unsigned integer U. Fails if I is negative.
+external pred coq.int->uint63 i:int, o:uint63.
+
 % [coq.float64->float F64 F] Transforms a primitive float on 64 bits to an
 % elpi one. Currently, it should not fail.
 external pred coq.float64->float i:float64, o:float.
 
+% [coq.float->float64 F F64] Transforms an elpi float F to a primitive float
+% on 64 bits. Currently, it should not fail.
+external pred coq.float->float64 i:float, o:float64.
+
 
 % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % API for extra logical objects
diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index c7f643175..0d354287b 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -2459,6 +2459,14 @@ declared as cumulative.|};
        else raise No_clause)),
   DocAbove);
 
+  MLCode(Pred("coq.int->uint63",
+    In(B.int,"I",
+    Out(Coq_elpi_utils.uint63,"U",
+    Easy "Transforms an elpi integer I into a primitive unsigned integer U. Fails if I is negative.")),
+    (fun i _ ~depth:_ ->
+       if i >= 0 then !: (Uint63.of_int i) else raise No_clause)),
+  DocAbove);
+
   MLCode(Pred("coq.float64->float",
     In(Coq_elpi_utils.float64,"F64",
     Out(B.float,"F",
@@ -2469,6 +2477,14 @@ declared as cumulative.|};
        with Failure _ -> raise No_clause)),
   DocAbove);
 
+  MLCode(Pred("coq.float->float64",
+    In(B.float,"F",
+    Out(Coq_elpi_utils.float64,"F64",
+    Easy "Transforms an elpi float F to a primitive float on 64 bits. Currently, it should not fail.")),
+    (fun f _ ~depth:_ ->
+       !: (Float64.of_float f))),
+  DocAbove);
+
   LPCode {|
 % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % API for extra logical objects
diff --git a/tests/test_API2.v b/tests/test_API2.v
index 6be8cc4b2..c884f7819 100644
--- a/tests/test_API2.v
+++ b/tests/test_API2.v
@@ -71,16 +71,28 @@ main X :- coq.error "not a primitive-value" X.
 }}.
 Elpi Typecheck.
 
+Elpi Command vp.
+Elpi Accumulate lp:{{
+
+main [int I] :- !, coq.say {coq.int->uint63 I}.
+main [] :- !, coq.say {coq.float->float64 1.2}.
+
+}}.
+Elpi Typecheck.
+
 From Coq Require Import PrimFloat Uint63.
 
 Open Scope uint63_scope.
 
 Elpi pv (1).
 Fail Elpi pv (4611686018427387904). (* max_int + 1 *)
+Elpi vp 1.
+Fail Elpi vp -1.
 
 Open Scope float_scope.
 
 Elpi pv (1.0).
+Elpi vp.
 
 Elpi Query lp:{{
 

From 2e9984b8ccd1b3cea0475c2aa5c091b2283c6eee Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Thu, 9 Mar 2023 11:08:29 +0100
Subject: [PATCH 8/8] clarify API for side effects

---
 src/coq_elpi_HOAS.ml     |  6 +--
 src/coq_elpi_builtins.ml | 82 ++++++++++++++++++++++------------------
 2 files changed, 48 insertions(+), 40 deletions(-)

diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml
index 2ac24f6a2..ee9d7d39d 100644
--- a/src/coq_elpi_HOAS.ml
+++ b/src/coq_elpi_HOAS.ml
@@ -789,8 +789,8 @@ let show_coq_engine ?with_univs e = Format.asprintf "%a" (pp_coq_engine ?with_un
 let from_env_keep_univ_of_sigma ~env0 ~env sigma0 =
    assert(env0 != env);
    let uctx = UState.update_sigma_univs (Evd.evar_universe_context sigma0) (Environ.universes env) in
-  let uctx = UState.demote_global_univs env uctx in
-  from_env_sigma env (Evd.from_ctx uctx)
+   let uctx = UState.demote_global_univs env uctx in
+   from_env_sigma env (Evd.from_ctx uctx)
  
  let init () = from_env (Global.env ())
 
@@ -2061,11 +2061,9 @@ let grab_global_env state =
   else
     if Environ.universes env0 == Environ.universes env then
       let state = S.set engine state (CoqEngine_HOAS.from_env_sigma env (get_sigma state)) in
-      (*let state = UVMap.empty state in*)
       state  
     else
       let state = S.set engine state (CoqEngine_HOAS.from_env_keep_univ_and_sigma ~env0 ~env (get_sigma state)) in
-      (*let state = UVMap.empty state in*)
       state
 let grab_global_env_drop_univs_and_sigma state =
   let env0 = get_global_env state in
diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index 0d354287b..0cfa6472e 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -109,16 +109,26 @@ let invocation_site_loc = State.declare ~name:"coq-elpi:invocation-site-loc"
   ~init:(fun () -> API.Ast.Loc.initial "(should-not-happen)")
   ~start:(fun x -> x)
 
-let on_global_state ?(abstract_exception=false) ?options api thunk = (); (fun state ->
-  if not abstract_exception && State.get tactic_mode state then
+let abstract__grab_global_env_keep_sigma api thunk = (); (fun state ->
+  let state, result, gls = thunk state in
+  Coq_elpi_HOAS.grab_global_env state, result, gls)
+
+let grab_global_env__drop_sigma_univs_if_option_is_set options 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 state, result, gls = thunk state in
   match options with
-  | Some { keepunivs = Some false } -> Coq_elpi_HOAS.grab_global_env_drop_univs_and_sigma state, result, gls
+  | { keepunivs = Some false } -> Coq_elpi_HOAS.grab_global_env_drop_univs_and_sigma state, result, gls
   | _ -> Coq_elpi_HOAS.grab_global_env state, result, gls)
 
+let grab_global_env 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 state, result, gls = thunk state in
+  Coq_elpi_HOAS.grab_global_env state, result, gls)
+
 (* This is for stuff that is not monotonic in the env, eg section closing *)
-let on_global_state_does_rewind_env api thunk = (); (fun state ->
+let grab_global_env_drop_sigma 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 state, result, gls = thunk state in
@@ -1774,7 +1784,7 @@ Supported attributes:
 - @udecl! (default unset)
 - @dropunivs! (default: false, drops all universe constraints from the store after the definition)
 |})))))),
-  (fun id body types opaque _ ~depth {options} _ -> on_global_state ~options "coq.env.add-const" (fun state ->
+  (fun id body types opaque _ ~depth {options} _ -> grab_global_env__drop_sigma_univs_if_option_is_set options "coq.env.add-const" (fun state ->
     let local = options.local = Some true in
     let state = minimize_universes state in
     (* Maybe: UState.nf_universes on body and type *)
@@ -1849,7 +1859,7 @@ Supported attributes:
 - @using! (default: section variables actually used)
 - @inline! (default: no inlining)
 - @inline-at! N (default: no inlining)|})))),
-  (fun id ty _ ~depth {options} _ -> on_global_state "coq.env.add-axiom" (fun state ->
+  (fun id ty _ ~depth {options} _ -> grab_global_env "coq.env.add-axiom" (fun state ->
      let gr = add_axiom_or_variable "coq.env.add-axiom" id ty false options state in
      state, !: (global_constant_of_globref gr), []))),
   DocAbove);
@@ -1860,7 +1870,7 @@ Supported attributes:
     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 {options} _ -> on_global_state "coq.env.add-section-variable" (fun state ->
+  (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), []))),
   DocAbove);
@@ -1872,7 +1882,7 @@ and the current module|})))),
 Supported attributes:
 - @dropunivs! (default: false, drops all universe constraints from the store after the definition)
 - @primitive! (default: false, makes records primitive)|}))),
-  (fun (me, uctx, univ_binders, record_info, ind_impls) _ ~depth {options} _ -> on_global_state ~options "coq.env.add-indt" (fun state ->
+  (fun (me, uctx, univ_binders, record_info, ind_impls) _ ~depth {options} _ -> grab_global_env__drop_sigma_univs_if_option_is_set options "coq.env.add-indt" (fun state ->
      let sigma = get_sigma state in
      if not (is_mutual_inductive_entry_ground me sigma) then
        err Pp.(str"coq.env.add-indt: the inductive type declaration must be ground. Did you forge to call coq.typecheck-indt-decl?");
@@ -1959,7 +1969,7 @@ with a number, starting from 1.
     In(option modtypath, "Its module type",
     In(list (pair id modtypath), "Parameters of the functor",
     Full(unit_ctx, "Starts a functor *E*")))),
-  (fun name mp binders_ast ~depth _ _ -> on_global_state "coq.env.begin-module-functor" (fun state ->
+  (fun name mp binders_ast ~depth _ _ -> grab_global_env "coq.env.begin-module-functor" (fun state ->
      if Global.sections_are_opened () then
        err Pp.(str"This elpi code cannot be run within a section since it opens a module");
      let ty =
@@ -1988,7 +1998,7 @@ coq.env.begin-module Name MP :-
   MLCode(Pred("coq.env.end-module",
     Out(modpath, "ModPath",
     Full(unit_ctx, "end the current module that becomes known as ModPath *E*")),
-  (fun _ ~depth _ _ -> on_global_state_does_rewind_env "coq.env.end-module" (fun state ->
+  (fun _ ~depth _ _ -> grab_global_env_drop_sigma "coq.env.end-module" (fun state ->
      let mp = Declaremods.end_module () in
      state, !: mp, []))),
   DocAbove);
@@ -1998,7 +2008,7 @@ coq.env.begin-module Name MP :-
     In(id, "The name of the functor",
     In(list (pair id modtypath), "The parameters of the functor",
     Full(unit_ctx,"Starts a module type functor *E*"))),
-  (fun id binders_ast ~depth _ _ -> on_global_state "coq.env.begin-module-type-functor" (fun state ->
+  (fun id binders_ast ~depth _ _ -> grab_global_env "coq.env.begin-module-type-functor" (fun state ->
      if Global.sections_are_opened () then
        err Pp.(str"This elpi code cannot be run within a section since it opens a module");
      let id = Id.of_string id in
@@ -2023,7 +2033,7 @@ coq.env.begin-module-type Name :-
   MLCode(Pred("coq.env.end-module-type",
     Out(modtypath, "ModTyPath",
     Full(unit_ctx, "end the current module type that becomes known as ModPath *E*")),
-  (fun _ ~depth _ _ -> on_global_state_does_rewind_env "coq.env.end-module-type" (fun state ->
+  (fun _ ~depth _ _ -> grab_global_env_drop_sigma "coq.env.end-module-type" (fun state ->
      let mp = Declaremods.end_modtype () in
      state, !: mp, []))),
   DocAbove);
@@ -2036,7 +2046,7 @@ coq.env.begin-module-type Name :-
     In(module_inline_default, "Arguments inlining",
     Out(modpath, "The modpath of the new module",
     Full(unit_ctx, "Applies a functor *E*"))))))),
-  (fun name mp f arguments inline _ ~depth _ _ -> on_global_state "coq.env.apply-module-functor" (fun state ->
+  (fun name mp f arguments inline _ ~depth _ _ -> grab_global_env "coq.env.apply-module-functor" (fun state ->
      if Global.sections_are_opened () then
        err Pp.(str"This elpi code cannot be run within a section since it defines a module");
      let ty =
@@ -2061,7 +2071,7 @@ coq.env.begin-module-type Name :-
     In(module_inline_default, "Arguments inlining",
     Out(modtypath, "The modtypath of the new module type",
     Full(unit_ctx, "Applies a type functor *E*")))))),
-  (fun name f arguments inline _ ~depth _ _ -> on_global_state "coq.env.apply-module-type-functor" (fun state ->
+  (fun name f arguments inline _ ~depth _ _ -> grab_global_env "coq.env.apply-module-type-functor" (fun state ->
      if Global.sections_are_opened () then
        err Pp.(str"This elpi code cannot be run within a section since it defines a module");
      let id = Id.of_string name in
@@ -2080,7 +2090,7 @@ coq.env.begin-module-type Name :-
     In(modpath, "ModPath",
     In(module_inline_default, "Inline",
     Full(unit_ctx, "is like the vernacular Include, Inline can be omitted *E*"))),
-  (fun mp inline ~depth _ _ -> on_global_state "coq.env.include-module" (fun state ->
+  (fun mp inline ~depth _ _ -> grab_global_env "coq.env.include-module" (fun state ->
      let fpath = match mp with
        | ModPath.MPdot(mp,l) ->
            Libnames.make_path (ModPath.dp mp) (Label.to_id l)
@@ -2096,7 +2106,7 @@ coq.env.begin-module-type Name :-
     In(modtypath, "ModTyPath",
     In(module_inline_default, "Inline",
     Full(unit_ctx, "is like the vernacular Include Type, Inline can be omitted  *E*"))),
-  (fun mp inline  ~depth _ _ -> on_global_state "coq.env.include-module-type" (fun state ->
+  (fun mp inline  ~depth _ _ -> grab_global_env "coq.env.include-module-type" (fun state ->
      let fpath = Nametab.path_of_modtype mp in
      let tname = Constrexpr.CMident (Libnames.qualid_of_path fpath) in
      let i = CAst.make tname, inline in
@@ -2107,7 +2117,7 @@ coq.env.begin-module-type Name :-
   MLCode(Pred("coq.env.import-module",
     In(modpath, "ModPath",
     Full(unit_ctx, "is like the vernacular Import *E*")),
-  (fun mp ~depth _ _ -> on_global_state "coq.env.import-module" (fun state ->
+  (fun mp ~depth _ _ -> grab_global_env "coq.env.import-module" (fun state ->
      Declaremods.import_module ~export:Lib.Import Libobject.unfiltered mp;
      state, (), []))),
   DocAbove);
@@ -2115,7 +2125,7 @@ coq.env.begin-module-type Name :-
   MLCode(Pred("coq.env.export-module",
     In(modpath, "ModPath",
     Full(unit_ctx, "is like the vernacular Export *E*")),
-  (fun mp ~depth _ _ -> on_global_state "coq.env.export-module" (fun state ->
+  (fun mp ~depth _ _ -> grab_global_env "coq.env.export-module" (fun state ->
      Declaremods.import_module ~export:Lib.Export Libobject.unfiltered mp;
      state, (), []))),
   DocAbove);
@@ -2139,7 +2149,7 @@ denote the same x as before.|};
   MLCode(Pred("coq.env.begin-section",
     In(id, "Name",
     Full(unit_ctx, "starts a section named Name *E*")),
-  (fun id ~depth _ _ -> on_global_state "coq.env.begin-section" (fun state ->
+  (fun id ~depth _ _ -> grab_global_env "coq.env.begin-section" (fun state ->
      let id = Id.of_string id in
      let lid = CAst.make ~loc:(to_coq_loc @@ State.get invocation_site_loc state) id in
      Dumpglob.dump_definition lid true "sec";
@@ -2149,7 +2159,7 @@ denote the same x as before.|};
 
   MLCode(Pred("coq.env.end-section",
     Full(unit_ctx, "end the current section *E*"),
-  (fun ~depth _ _ -> on_global_state_does_rewind_env "coq.env.end-section" (fun state ->
+  (fun ~depth _ _ -> grab_global_env_drop_sigma "coq.env.end-section" (fun state ->
      let loc = to_coq_loc @@ State.get invocation_site_loc state in
      Dumpglob.dump_reference ~loc
        (DirPath.to_string (Lib.current_dirpath true)) "<>" "sec";
@@ -2500,7 +2510,7 @@ declared as cumulative.|};
     Full(global, {|Declares GR as a canonical structure instance.
 Supported attributes:
 - @local! (default: false)|})),
-  (fun gr ~depth { options } _ -> on_global_state "coq.CS.declare-instance" (fun state ->
+  (fun gr ~depth { options } _ -> grab_global_env "coq.CS.declare-instance" (fun state ->
      Canonical.declare_canonical_structure ?local:options.local gr;
     state, (), []))),
   DocAbove);
@@ -2538,7 +2548,7 @@ Supported attributes:
   MLCode(Pred("coq.TC.declare-class",
     In(gref, "GR",
     Full(global, {|Declare GR as a type class|})),
-  (fun gr ~depth { options } _ -> on_global_state "coq.TC.declare-class" (fun state ->
+  (fun gr ~depth { options } _ -> grab_global_env "coq.TC.declare-class" (fun state ->
      Record.declare_existing_class gr;
      state, (), []))),
   DocAbove);
@@ -2551,7 +2561,7 @@ Supported attributes:
     Full(global, {|Declare GR as a Global type class instance with Priority.
 Supported attributes:
 - @global! (default: true)|}))),
-  (fun gr priority ~depth { options } _ -> on_global_state "coq.TC.declare-instance" (fun state ->
+  (fun gr priority ~depth { options } _ -> grab_global_env "coq.TC.declare-instance" (fun state ->
      let global = if options.local = Some false then Hints.SuperGlobal else Hints.Local in
      let hint_priority = Some priority in
      let qualid =
@@ -2596,7 +2606,7 @@ NParams can always be omitted, since it is inferred.
 - @global! (default: false)
 - @nonuniform! (default: false)
 - @reversible! (default: false)|})),
-  (fun (gr, _, source, target) ~depth { options } _ -> on_global_state "coq.coercion.declare" (fun state ->
+  (fun (gr, _, source, target) ~depth { options } _ -> grab_global_env "coq.coercion.declare" (fun state ->
      let local = options.local <> Some false in
      let poly = false in
      let nonuniform = options.nonuniform = Some true in
@@ -2668,7 +2678,7 @@ This old behavior is available via the @global! flag, but is discouraged.
     In(B.list mode, "Mode",
     Full(global, {|Adds a mode declaration to DB about GR.
 Supported attributes:|} ^ hint_locality_doc)))),
-  (fun gr (db,_) mode ~depth:_ {options} _ -> on_global_state "coq.hints.add-mode" (fun state ->
+  (fun gr (db,_) mode ~depth:_ {options} _ -> grab_global_env "coq.hints.add-mode" (fun state ->
      let locality = hint_locality options in
      Hints.add_hints ~locality [db] (Hints.HintsModeEntry(gr,mode));
      state, (), []
@@ -2695,7 +2705,7 @@ Supported attributes:|} ^ hint_locality_doc)))),
     In(B.bool, "Opaque",
     Full(global,{|Like Hint Opaque C : DB (or Hint Transparent, if the boolean is ff).
 Supported attributes:|} ^ hint_locality_doc)))),
-  (fun c (db,_) opaque ~depth:_ {options} _ -> on_global_state "coq.hints.set-opaque" (fun state ->
+  (fun c (db,_) opaque ~depth:_ {options} _ -> grab_global_env "coq.hints.set-opaque" (fun state ->
     let locality = hint_locality options in
     let transparent = not opaque in
     let r = match c with
@@ -2725,7 +2735,7 @@ Supported attributes:|} ^ hint_locality_doc)))),
   CIn(B.unspecC closed_term, "Pattern",
   Full(global,{|Like Hint Resolve GR | Priority Pattern : DB.
 Supported attributes:|} ^ hint_locality_doc))))),
-(fun gr (db,_) priority pattern ~depth:_ {env;options} _ -> on_global_state "coq.hints.add-resolve" (fun state ->
+(fun gr (db,_) priority pattern ~depth:_ {env;options} _ -> grab_global_env "coq.hints.add-resolve" (fun state ->
   let locality = hint_locality options in
   let hint_priority = unspec2opt priority in
   let sigma = get_sigma state in
@@ -2761,7 +2771,7 @@ Unspecified means explicit.
 See also the [] and {} flags for the Arguments command.
 Supported attributes:
 - @global! (default: false)|}))),
-  (fun gref imps ~depth {options} _ -> on_global_state "coq.arguments.set-implicit" (fun state ->
+  (fun gref imps ~depth {options} _ -> grab_global_env "coq.arguments.set-implicit" (fun state ->
      let local = options.local <> Some false in
      let imps = imps |> List.(map (map (function
        | B.Unspec -> Anonymous, Glob_term.Explicit
@@ -2777,7 +2787,7 @@ Supported attributes:
 See also the "default implicits" flag to the Arguments command.
 Supported attributes:
 - @global! (default: false)|})),
-  (fun gref ~depth { options } _ -> on_global_state "coq.arguments.set-default-implicit" (fun state ->
+  (fun gref ~depth { options } _ -> grab_global_env "coq.arguments.set-default-implicit" (fun state ->
      let local = options.local <> Some false in
      Impargs.declare_implicits local gref;
      state, (), []))),
@@ -2802,7 +2812,7 @@ Supported attributes:
 See also the :rename flag to the Arguments command.
 Supported attributes:
 - @global! (default: false)|}))),
-  (fun gref names ~depth { options } _ -> on_global_state "coq.arguments.set-name" (fun state ->
+  (fun gref names ~depth { options } _ -> grab_global_env "coq.arguments.set-name" (fun state ->
      let local = options.local <> Some false in
      let names = names |> List.map (function
        | None -> Names.Name.Anonymous
@@ -2827,7 +2837,7 @@ Scope can be a scope name or its delimiter.
 See also the %scope modifier for the Arguments command.
 Supported attributes:
 - @global! (default: false)|}))),
-  (fun gref scopes ~depth { options } _ -> on_global_state "coq.arguments.set-scope" (fun state ->
+  (fun gref scopes ~depth { options } _ -> grab_global_env "coq.arguments.set-scope" (fun state ->
      let local = options.local <> Some false in
      let scopes = scopes |> List.map (List.map (fun k ->
         try ignore (CNotation.find_scope k); k
@@ -2855,7 +2865,7 @@ Positions are 0 based.
 See also the ! and / modifiers for the Arguments command.
 Supported attributes:
 - @global! (default: false)|}))),
-  (fun gref strategy ~depth { options } _ -> on_global_state "coq.arguments.set-simplification" (fun state ->
+  (fun gref strategy ~depth { options } _ -> grab_global_env "coq.arguments.set-simplification" (fun state ->
      let local = options.local <> Some false in
      Reductionops.ReductionBehaviour.set ~local gref strategy;
      state, (), []))),
@@ -2886,7 +2896,7 @@ The term must begin with at least Nargs "fun" nodes whose domain is ignored, eg
 Supported attributes:
 - @deprecated! (default: not deprecated)
 - @global! (default: false)|})))))),
-  (fun name nargs term onlyparsing _ ~depth { env; options } _ -> on_global_state "coq.notation.add-abbreviation" (fun state ->
+  (fun name nargs term onlyparsing _ ~depth { env; options } _ -> grab_global_env "coq.notation.add-abbreviation" (fun state ->
        let sigma = get_sigma state in
        let strip_n_lambas nargs env term =
        let rec aux vars nenv env n t =
@@ -3006,7 +3016,7 @@ at which the term is written (unlike if a regular abbreviation was
 declared by hand).
 A call to coq.notation.add-abbreviation-for-tactic TacName TacName []
 is equivalent to Elpi Export TacName.|})))),
-    (fun name tacname more_args ~depth { options} _ -> on_global_state "coq.notation.add-abbreviation-for-tactic" (fun state ->
+    (fun name tacname more_args ~depth { options} _ -> grab_global_env "coq.notation.add-abbreviation-for-tactic" (fun state ->
       let sigma = get_sigma state in
       let env = get_global_env state in
       let tac_fixed_args = more_args |> List.map (function
@@ -3361,7 +3371,7 @@ coq.reduction.lazy.whd_all X Y :-
     In(B.list constant, "CL",
     In(conversion_strategy, "Level",
     Full(global,"Sets the unfolding priority for all the constants in the list CL. See the command Strategy."))),
-    (fun csts level ~depth:_ ctx _ -> on_global_state "coq.strategy.set" (fun state ->
+    (fun csts level ~depth:_ ctx _ -> grab_global_env "coq.strategy.set" (fun state ->
        let local = ctx.options.local = Some true in
        let csts = csts |> List.map (function
          | Constant c -> Tacred.EvalConstRef c
@@ -3451,7 +3461,7 @@ fold_left over the terms, letin body comes before the type).
     CIn(goal, "G",
     Out(list sealed_goal,"GL",
     Full(raw_ctx, "Calls Ltac1 tactic named Tac on goal G (passing the arguments of G, see coq.ltac.call for a handy wrapper)")))),
-    (fun tac_name (proof_context,goal,tac_args) _ ~depth _ _ -> on_global_state ~abstract_exception:true "coq.ltac.call-ltac1" (fun state ->
+    (fun tac_name (proof_context,goal,tac_args) _ ~depth _ _ -> abstract__grab_global_env_keep_sigma "coq.ltac.call-ltac1" (fun state ->
       let open Ltac_plugin in
       let sigma = get_sigma state in
        let tac_args = tac_args |> List.map (function