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/_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/coq-builtin.elpi b/coq-builtin.elpi
index f37c2b181..3fa442dbf 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_HOAS.ml b/src/coq_elpi_HOAS.ml
index 79d853dc2..ee9d7d39d 100644
--- a/src/coq_elpi_HOAS.ml
+++ b/src/coq_elpi_HOAS.ml
@@ -752,21 +752,19 @@ 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
 
   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 } =
@@ -782,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 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.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 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 =
@@ -1992,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
@@ -2043,14 +2051,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 *)
@@ -2060,22 +2060,29 @@ 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
       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
       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"
@@ -2112,8 +2119,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 +2152,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 +3422,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..7aee54b44 100644
--- a/src/coq_elpi_HOAS.mli
+++ b/src/coq_elpi_HOAS.mli
@@ -255,9 +255,9 @@ 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
+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 *)
@@ -265,11 +265,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_builtins.ml b/src/coq_elpi_builtins.ml
index be9ccd7b2..c0e649dea 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -109,20 +109,30 @@ 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 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
-  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
@@ -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 "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 "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";
@@ -2459,6 +2469,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 +2487,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
@@ -2484,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);
@@ -2522,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);
@@ -2535,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 =
@@ -2580,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
@@ -2652,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, (), []
@@ -2679,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
@@ -2709,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
@@ -2745,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
@@ -2761,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, (), []))),
@@ -2786,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
@@ -2811,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
@@ -2839,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, (), []))),
@@ -2870,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 =
@@ -2990,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
@@ -3345,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
@@ -3435,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
@@ -3476,7 +3502,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/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml
index de0256fbf..08f522a00 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)
@@ -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)
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:{{
 
diff --git a/tests/test_ltac3.v b/tests/test_ltac3.v
new file mode 100644
index 000000000..c925d2596
--- /dev/null
+++ b/tests/test_ltac3.v
@@ -0,0 +1,24 @@
+
+From elpi Require Export elpi.
+From Coq Require Import ssreflect ssrfun ssrbool.
+
+Ltac ltac_foo := cut True; [ idtac | abstract (exact I) ].
+
+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 nat.
+Proof.
+elpi fail_foo ([the fooType of unit : Type]).
+exact (fun _ => 0).
+Qed.