diff --git a/.nix/config.nix b/.nix/config.nix
index 01d61300b..a7e4fdd7f 100644
--- a/.nix/config.nix
+++ b/.nix/config.nix
@@ -14,7 +14,7 @@ let master = [
     "trakt"
   ];
   rocq-common-bundles = {
-    rocq-elpi.override.elpi-version = "3.4.2";
+    rocq-elpi.override.elpi-version = "improve-overload-resolution";
     hierarchy-builder.override.version = "master";
     rocq-elpi-tests.job = true;
     rocq-elpi-tests-stdlib.job = true;
@@ -22,7 +22,7 @@ let master = [
   coq-common-bundles = listToAttrs (forEach master (p:
     { name = p; value.override.version = "master"; }))
   // {
-    coq-elpi.override.elpi-version = "3.4.2";
+    coq-elpi.override.elpi-version = "improve-overload-resolution";
 
     mathcomp-boot.job = true;
     mathcomp-fingroup.job = true;
diff --git a/Changelog.md b/Changelog.md
index a71720b7d..e4287db5f 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,5 +1,7 @@
 # Unreleased
 
+Requires Elpi 3.6.0 and Rocq 9.0, 9.1 or 9.2.
+
 ### HOAS:
 - Fix explicitly declared goals are considered reachable, even if they
   do not occur in the proof term
@@ -13,6 +15,12 @@
 - New `coq.env.section-contents` listing the contents of sections.
 - New `coq.ltac.call-mltac` to call code defined via `TACTIC EXTEND` directives
   in OCaml.
+- New `coq.ltac.call-simple-mltac` for tactics not changing the proof context
+- New `coq.ltac.call-simple-ltac1` for tactics not changing the proof context
+- Rename `coq.ltac.collect-goals` -> `coq.ltac.collect-sealed-goals`
+- New `coq.ltac.collect-simple-goals` for goals in the current proof context
+- Change `coq.ltac.call-ltac1` also gives a diagnostic
+- Change `coq.ltac.call` also gives a diagnostic
 
 # [3.2.0] 19/09/2025
 
diff --git a/apps/coercion/README.md b/apps/coercion/README.md
index f5a45aa11..6243986b5 100644
--- a/apps/coercion/README.md
+++ b/apps/coercion/README.md
@@ -61,7 +61,7 @@ coercion _ X Ty {{ @sig lp:Ty lp:P }} Solution :- std.do! [
   Solution = {{ @exist lp:Ty lp:P lp:X1 _ }},
   % we call the solver
   coq.ltac.collect-goals Solution [G] [],
-  coq.ltac.open (coq.ltac.call-ltac1 "my_solver") G [],
+  coq.ltac.open (x\y\coq.ltac.call-ltac1 "my_solver" x y ok) G [],
 ].
 
 }}.
diff --git a/apps/coercion/tests/test_open.v b/apps/coercion/tests/test_open.v
index 228582a58..d262ca11e 100644
--- a/apps/coercion/tests/test_open.v
+++ b/apps/coercion/tests/test_open.v
@@ -12,7 +12,7 @@ coercion _ X Ty {{ @sig lp:Ty lp:P }} Solution :- std.do! [
   Solution = {{ @exist lp:Ty lp:P lp:X1 _ }},
   % we call the solver
   coq.ltac.collect-goals Solution [G] [],
-  coq.ltac.open (coq.ltac.call-ltac1 "my_solver") G [],
+  coq.ltac.open (x\y\coq.ltac.call-ltac1 "my_solver" x y ok) G [],
 ].
 
 }}.
diff --git a/apps/derive/elpi/eqbcorrect.elpi b/apps/derive/elpi/eqbcorrect.elpi
index 7f975e4b4..1b853784a 100644
--- a/apps/derive/elpi/eqbcorrect.elpi
+++ b/apps/derive/elpi/eqbcorrect.elpi
@@ -128,7 +128,7 @@ search-eqcorrect-apply (eqb.inductive _ _) [] C R C R.
 
 func run-solver sealed-goal, string ->.
 run-solver G Name :-
-  if (coq.ltac.open (coq.ltac.call Name []) G []) true
+  if (coq.ltac.open (g\gl\coq.ltac.call Name [] g gl ok) G []) true
      ((@holes! => coq.sealed-goal->string G SG),
       std.fatal-error {calc ( "solver " ^ Name ^ " fails on goal:\n" ^ SG )}).
 
diff --git a/builtin-doc/coq-builtin.elpi b/builtin-doc/coq-builtin.elpi
index 820b6b710..0c1af60c3 100644
--- a/builtin-doc/coq-builtin.elpi
+++ b/builtin-doc/coq-builtin.elpi
@@ -1634,7 +1634,7 @@ kind ltac1-tactic type.
 % Level can be left unspecified and defaults to 0
 external type coq.ltac.fail int -> variadic any (func).
 
-% [coq.ltac.collect-goals T Goals ShelvedGoals] 
+% [coq.ltac.collect-sealed-goals T Goals ShelvedGoals] 
 % Turns the holes in T into Goals.
 % Goals are closed with nablas.
 % ShelvedGoals are goals which can be solved by side effect (they occur
@@ -1643,11 +1643,23 @@ external type coq.ltac.fail int -> variadic any (func).
 % (a
 % fold_left over the terms, letin body comes before the type).
 % 
-external func coq.ltac.collect-goals term -> list sealed-goal, 
-                                    list sealed-goal.
+external func coq.ltac.collect-sealed-goals term -> list sealed-goal, 
+                                           list sealed-goal.
 
-% [coq.ltac.call-mltac PluginName BlockName BlockIndex G GL] Calls OCaml
-% code bound via TACTIC EXTEND. For example the
+
+func coq.ltac.collect-goals term -> list sealed-goal, list sealed-goal.
+coq.ltac.collect-goals T GA GB :- coq.ltac.collect-sealed-goals T GA GB.
+
+
+% [coq.ltac.collect-simple-goals T Goals ShelvedGoals] Like
+% coq.ltac.collect-sealed-goals turns the holes in T into
+% Goals but fails if the goals do not live in the current proof context.
+% 
+external func coq.ltac.collect-simple-goals term -> list goal, 
+                                           list sealed-goal.
+
+% [coq.ltac.call-mltac PluginName BlockName BlockIndex G GL Diagnostic]
+% Calls OCaml code bound via TACTIC EXTEND. For example the
 % OCaml code for lia looks like:
 % 
 %   DECLARE PLUGIN "rocq-runtime.plugins.micromega"
@@ -1665,13 +1677,27 @@ external func coq.ltac.collect-goals term -> list sealed-goal,
 % numbering
 % starts from 0. Also, each block has a name, "Lia" in this case.
 %     
+% When the diagnostic is (error Msg), then GL is not set.
+% 
 % Supported attributes:
 % - @no-tc! (default false, do not infer typeclasses)
 external func coq.ltac.call-mltac string, string, int, 
-                                 goal -> list sealed-goal.
+                                 goal -> list sealed-goal, diagnostic.
 
-% [coq.ltac.call-ltac1 Tac G GL] Calls Ltac1 tactic Tac on goal G (passing
-% the arguments of G, see coq.ltac.call for a handy wrapper).
+% [coq.ltac.call-simple-mltac PluginName BlockName BlockIndex G GL
+% Diagnostic] Like coq.ltac.call-mltac but Tac is not allowed to
+% generate new goals GL in different contexts. For example "intro" does
+% not
+% obey this restriction.
+% 
+% Supported attributes:
+% - @no-tc! (default false, do not infer typeclasses)
+external func coq.ltac.call-simple-mltac string, string, int, 
+                                        goal -> list goal, diagnostic.
+
+% [coq.ltac.call-ltac1 Tac G GL ...] Calls Ltac1 tactic Tac on goal G
+% (passing the arguments of G, see coq.ltac.call for a handy wrapper).
+% It accepts one diagnostic argument, defaults to ok if omitted.
 % Tac can either be a string (the tactic name), or a value
 % of type ltac1-tactic, see the tac argument constructor
 % and the ltac_tactic:(...) syntax to pass arguments to
@@ -1681,9 +1707,24 @@ external func coq.ltac.call-mltac string, string, int,
 %   "Ltac name := body", it cannot be a builtin one. For example
 %   "Ltac myapply x := apply x." lets one call apply by running
 %   coq.ltac.call-ltac1 "myapply" G GL.
+% 
+% When the diagnostic is (error Msg), then GL is not set.
+% 
+% Supported attributes:
+% - @no-tc! (default false, do not infer typeclasses)
+external func coq.ltac.call-ltac1 any, goal -> list sealed-goal, 
+                                 diagnostic.. .
+
+% [coq.ltac.call-simple-ltac1 Tac G GL Diagnostic] Like coq.ltac.call-ltac1
+% but Tac is not allowed to
+% generate new goals GL in different contexts. For example "intro" does
+% not
+% obey this restriction.
+% 
 % Supported attributes:
 % - @no-tc! (default false, do not infer typeclasses)
-external func coq.ltac.call-ltac1 any, goal -> list sealed-goal.
+external func coq.ltac.call-simple-ltac1 any, goal -> list goal, 
+                                        diagnostic.
 
 % [coq.ltac.id-free? ID G] 
 %     Fails if ID is already used in G. Note that ids which are taken are
diff --git a/builtin-doc/elpi-builtin.elpi b/builtin-doc/elpi-builtin.elpi
index cf2bb7420..7127be336 100644
--- a/builtin-doc/elpi-builtin.elpi
+++ b/builtin-doc/elpi-builtin.elpi
@@ -14,9 +14,14 @@ func fail.
 
 func false.
 
-external func (=) -> A, A. % unification term term
 
-external func pattern_match A -> A. % matching pattern term
+% [X = T] unifies X with Y, possibly assigning unification
+% variables in X and Y.
+external func (=) -> A, A.
+
+% [pattern_matching T P] matches T against pattern P, only
+% variables in P are assigned.
+external func pattern_match A -> A.
 
 external func (pi) (func A).
 
@@ -368,6 +373,11 @@ external func same_term A, A.
 func (==) A, A.
 X == Y :- same_term X Y.
 
+% Unification without occur check. It can create infinite terms.
+:nooc
+func unsound_unif -> A, A.
+unsound_unif X X.
+
 
 % [cmp_term A B Cmp] Compares A and B. Only works if A and B are ground.
 external func cmp_term any, any -> cmp.
@@ -1182,6 +1192,136 @@ bindings (node L V D R _) X X1 :-
 } % std.map.private
 } % std.map
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% Fast maps only work ground terms but do not perform occur check
+
+kind std.fmap type -> type -> type.
+type std.fmap std.fmap.private.map K V -> (func K, K -> cmp) -> std.fmap K V.
+
+namespace std.fmap {
+
+% [make Eq Ltn M] builds an empty map M where keys are compared using Eq and Ltn
+func make (func K, K -> cmp) -> std.fmap K V.
+make Cmp (std.fmap private.empty Cmp).
+
+% [find K M V] looks in M for the value V associated to K
+func find K, std.fmap K V -> V.
+find K (std.fmap M Cmp) V :-
+  private.assert-ground K,
+  private.find M Cmp K V.
+
+% [add K V M M1] M1 is M where K is bound to V
+func add K, V, std.fmap K V -> std.fmap K V.
+add K V (std.fmap M Cmp) R :-
+  private.assert-ground K,
+  private.assert-ground V,
+  private.add M Cmp K V M1,
+  unsound_unif R (std.fmap M1 Cmp).
+
+% [remove K M M1] M1 is M where K is unbound
+func remove K, std.fmap K V -> std.fmap K V.
+remove K (std.fmap M Cmp) R :-
+  private.assert-ground K,
+  private.remove M Cmp K M1,
+  unsound_unif R (std.fmap M1 Cmp).
+
+% [bindings M L] L is the key-value pairs in increasing order
+func bindings std.fmap K V -> list (pair K V).
+bindings (std.fmap M _) L :- private.bindings M [] L.
+
+namespace private {
+
+func assert-ground A.
+assert-ground A :- std.assert! (ground_term A) "std.fmap: not ground".
+
+% Taken from OCaml's map.ml
+kind map type -> type -> type.
+type empty map K V.
+type node map K V -> K -> V -> map K V -> int -> map K V.
+
+func height map K V -> int.
+height empty 0.
+height (node _ _ _ _ H) H.
+
+func create map K V, K, V, map K V -> map K V.
+create L K V R X :-
+  H is {std.max {height L} {height R}} + 1,
+  unsound_unif X (node L K V R H).
+
+func bal map K V, K, V, map K V -> map K V.
+bal L K V R T :-
+  height L HL,
+  height R HR,
+  HL2 is HL + 2,
+  HR2 is HR + 2,
+  bal.aux HL HR HL2 HR2 L K V R T.
+
+func bal.aux int, int, int, int, map K V, K, V, map K V -> map K V.
+bal.aux HL _ _ HR2 (node LL LV LD LR _) X D R T :-
+  HL > HR2, {height LL} >= {height LR}, !,
+  create LL LV LD {create LR X D R} T.
+bal.aux HL _ _ HR2 (node LL LV LD (node LRL LRV LRD LRR _) _) X D R T :-
+  HL > HR2, !,
+  create {create LL LV LD LRL} LRV LRD {create LRR X D R} T.
+bal.aux _ HR HL2 _ L X D (node RL RV RD RR _) T :-
+  HR > HL2, {height RR} >= {height RL}, !,
+  create {create L X D RL} RV RD RR T.
+bal.aux _ HR HL2 _ L X D (node (node RLL RLV RLD RLR _) RV RD RR _) T :-
+  HR > HL2, !,
+  create {create L X D RLL} RLV RLD {create RLR RV RD RR} T.
+bal.aux _ _ _ _ L K V R T :- create L K V R T.
+
+func add map K V, (func K, K -> cmp), K, V -> map K V.
+add empty _ K V T :- create empty K V empty T.
+add (node _ X _ _ _ as M) Cmp X1 XD M1 :- Cmp X1 X E, add.aux E M Cmp X1 XD M1.
+
+func add.aux cmp, map K V, (func K, K -> cmp), K, V -> map K V.
+add.aux eq (node L _ _ R H) _   X XD T :- unsound_unif T (node L X XD R H). 
+add.aux lt (node L V D R _) Cmp X XD T :- bal {add L Cmp X XD} V D R T.
+add.aux gt (node L V D R _) Cmp X XD T :- bal L V D {add R Cmp X XD} T.
+
+func find map K V, (func K, K -> cmp), K -> V.
+find (node L K1 V1 R _) Cmp K V :- Cmp K K1 E, find.aux E Cmp L R V1 K V.
+
+func find.aux cmp, (func K, K -> cmp), map K V, map K V, V, K -> V.
+find.aux eq _   _ _ V _ V.
+find.aux lt Cmp L _ _ K V :- find L Cmp K V.
+find.aux gt Cmp _ R _ K V :- find R Cmp K V.
+
+func remove-min-binding map K V -> map K V.
+remove-min-binding (node empty _ _ R _) R :- !.
+remove-min-binding (node L V D R _) X :- bal {remove-min-binding L} V D R X.
+
+func min-binding map K V -> K, V.
+min-binding (node empty V D _ _) V D :- !.
+min-binding (node L _ _ _ _) V D :- min-binding L V D.
+
+func merge map K V, map K V -> map K V.
+merge empty X X :- !.
+merge X empty X :- !.
+merge M1 M2 R :-
+  min-binding M2 X D,
+  bal M1 X D {remove-min-binding M2} R.
+
+func remove map K V, (func K, K -> cmp), K -> map K V.
+remove empty _ _ empty :- !.
+remove (node L V D R _) Cmp X M :- Cmp X V E, remove.aux E Cmp L R V D X M.
+
+func remove.aux cmp, (func K, K -> cmp), map K V, map K V, K, V, K -> map K V.
+remove.aux eq _   L R _ _ _ M :- merge L R M.
+remove.aux lt Cmp L R V D X M :- bal {remove L Cmp X} V D R M.
+remove.aux gt Cmp L R V D X M :- bal L V D {remove R Cmp X} M.
+
+func bindings map K V, list (pair K V) -> list (pair K V).
+bindings empty X X.
+bindings (node L V D R _) X X1 :-
+  bindings L [pr V D|{bindings R X}] X1.
+
+
+} % std.fmap.private
+} % std.fmap
+
 
 #line 1 "builtin_set.elpi"
 kind std.set type -> type.
@@ -1302,6 +1442,139 @@ elements (node L E R _) Acc X :-
 } % std.set.private
 } % std.set
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% Fast sets only work ground terms but do not perform occur check
+
+kind std.fset type -> type.
+type std.fset std.fset.private.set E -> (func E, E -> cmp) -> std.fset E.
+
+namespace std.fset {
+
+% [make Eq Ltn M] builds an empty set M where keys are compared using Eq and Ltn
+func make (func E, E -> cmp) -> std.fset E.
+make Cmp (std.fset private.empty Cmp).
+
+% [mem E M] looks if E is in M
+func mem E, std.fset E.
+mem E (std.fset M Cmp):- private.mem M Cmp E.
+
+% [add E M M1] M1 is M + {E}
+func add E, std.fset E -> std.fset E.
+add E (std.fset M Cmp) R :-
+  private.assert-ground E,
+  private.add M Cmp E M1,
+  unsound_unif R (std.fset M1 Cmp).
+
+% [remove E M M1] M1 is M - {E}
+func remove E, std.fset E -> std.fset E.
+remove E (std.fset M Cmp) R :-
+  private.assert-ground E,
+  private.remove M Cmp E M1,
+  unsound_unif R (std.fset M1 Cmp).
+
+% [cardinal S N] N is the number of elements of S
+func cardinal std.fset E -> int.
+cardinal (std.fset M _) N :- private.cardinal M N.
+
+func elements std.fset E -> list E.
+elements (std.fset M _) L :- private.elements M [] L.
+
+namespace private {
+
+func assert-ground A.
+assert-ground A :- std.assert! (ground_term A) "std.fset: not ground".
+
+% Taken from OCaml's set.ml
+kind set type -> type.
+type empty set E.
+type node set E -> E -> set E -> int -> set E.
+
+func height set E -> int.
+height empty 0.
+height (node _ _ _ H) H.
+
+func create set E, E, set E -> set E.
+create L E R S :-
+  H is {std.max {height L} {height R}} + 1,
+  unsound_unif S (node L E R H).
+
+func bal set E, E, set E -> set E.
+bal L E R T :-
+  height L HL,
+  height R HR,
+  HL2 is HL + 2,
+  HR2 is HR + 2,
+  bal.aux HL HR HL2 HR2 L E R T.
+
+func bal.aux int, int, int, int, set E, E, set E -> set E.
+bal.aux HL _ _ HR2 (node LL LV LR _) X R T :-
+  HL > HR2, {height LL} >= {height LR}, !,
+  create LL LV {create LR X R} T.
+bal.aux HL _ _ HR2 (node LL LV (node LRL LRV LRR _) _) X R T :-
+  HL > HR2, !,
+  create {create LL LV LRL} LRV {create LRR X R} T.
+bal.aux _ HR HL2 _ L X (node RL RV RR _) T :-
+  HR > HL2, {height RR} >= {height RL}, !,
+  create {create L X RL} RV RR T.
+bal.aux _ HR HL2 _ L X (node (node RLL RLV RLR _) RV RR _) T :-
+  HR > HL2, !,
+  create {create L X RLL} RLV {create RLR RV RR} T.
+bal.aux _ _ _ _ L E R T :- create L E R T.
+
+func add set E, (func E, E -> cmp), E -> set E.
+add empty _ E T :- create empty E empty T.
+add (node L X R H) Cmp X1 S :- Cmp X1 X E, add.aux E Cmp L R X X1 H S.
+
+func add.aux cmp, (func E, E -> cmp), set E, set E, E, E, int -> set E.
+add.aux eq _   L R X _ H S :- unsound_unif S (node L X R H).
+add.aux lt Cmp L R E X _ T :- bal {add L Cmp X} E R T.
+add.aux gt Cmp L R E X _ T :- bal L E {add R Cmp X} T.
+
+func mem set E, (func E, E -> cmp), E.
+mem (node L K R _) Cmp E :- Cmp E K O, mem.aux O Cmp L R E.
+
+func mem.aux cmp, (func E, E -> cmp), set E, set E, E.
+mem.aux eq _ _ _ _.
+mem.aux lt Cmp L _ E :- mem L Cmp E.
+mem.aux gt Cmp _ R E :- mem R Cmp E.
+
+func remove-min-binding set E -> set E.
+remove-min-binding (node empty _ R _) R :- !.
+remove-min-binding (node L E R _) X :- bal {remove-min-binding L} E R X.
+
+func min-binding set E -> E.
+min-binding (node empty E _ _) E :- !.
+min-binding (node L _ _ _) E :- min-binding L E.
+
+func merge set E, set E -> set E.
+merge empty X X :- !.
+merge X empty X :- !.
+merge M1 M2 R :-
+  min-binding M2 X,
+  bal M1 X {remove-min-binding M2} R.
+
+func remove set E, (func E, E -> cmp), E -> set E.
+remove empty _ _ empty.
+remove (node L E R _) Cmp X M :- Cmp X E O, remove.aux O Cmp L R E X M.
+
+func remove.aux cmp, (func E, E -> cmp), set E, set E, E, E -> set E.
+remove.aux eq _   L R _ _ M :- merge L R M.
+remove.aux lt Cmp L R E X M :- bal {remove L Cmp X} E R M.
+remove.aux gt Cmp L R E X M :- bal L E {remove R Cmp X} M.
+
+func cardinal set E -> int.
+cardinal empty 0.
+cardinal (node L _ R _) N :- N is {cardinal L} + 1 + {cardinal R}.
+
+func elements set E, list E -> list E.
+elements empty X X.
+elements (node L E R _) Acc X :-
+  elements L [E|{elements R Acc}] X.
+
+} % std.fset.private
+} % std.fset
+
 
 %  == I/O builtins =====================================
 
diff --git a/elpi/elpi-ltac.elpi b/elpi/elpi-ltac.elpi
index 9b02396a5..8ae58ad73 100644
--- a/elpi/elpi-ltac.elpi
+++ b/elpi/elpi-ltac.elpi
@@ -1,9 +1,13 @@
 /* elpi-ltac: building blocks for tactics                                    */
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
-typeabbrev tactic (pred i:sealed-goal, o:list sealed-goal).
+typeabbrev tactic (pred sealed-goal -> list sealed-goal).
 typeabbrev func-tactic (func sealed-goal -> list sealed-goal).
-typeabbrev open-tactic (pred i:goal, o:list sealed-goal).
+
+typeabbrev simple-tactic (pred goal -> list goal).
+typeabbrev func-simple-tactic (func goal -> list goal).
+
+typeabbrev open-tactic (pred goal -> list sealed-goal).
 typeabbrev func-open-tactic (func goal -> list sealed-goal).
 
 % The one tactic ------------------------------------------------------------
@@ -18,6 +22,14 @@ refine.elaborate T (goal _ RawEv Ty Ev _) GS :-
   RawEv = T,
   Ev = TR.
 
+func refine.simple-elaborate term, goal -> list goal.
+refine.simple-elaborate T (goal _ RawEv Ty Ev _) GS :-
+  rm-evar RawEv Ev,
+  (@keepunivs! => coq.elaborate-skeleton T Ty TR ok),
+  coq.ltac.collect-simple-goals TR GS _,
+  RawEv = T,
+  Ev = TR.
+
 func refine.typecheck term, goal -> list sealed-goal.
 refine.typecheck T (goal _ RawEv Ty Ev _) GS :-
   rm-evar RawEv Ev,
@@ -36,14 +48,24 @@ refine.no_check T (goal _ RawEv _ Ev _) GS :-
 % calling other tactics, with arguments ---------------------------------------
 
 func coq.ltac string, sealed-goal -> list sealed-goal.
-coq.ltac Tac G GS :- coq.ltac.open (coq.ltac.call-ltac1 Tac) G GS.
+coq.ltac Tac G GS :- coq.ltac.open (x\y\coq.ltac.call-ltac1 Tac x y ok) G GS.
 
 namespace coq.ltac {
 
+func call string, list argument, goal -> list sealed-goal, diagnostic.
+call Tac Args G GS D :-
+  set-goal-arguments Args G (seal G) (seal G1),
+  coq.ltac.call-ltac1 Tac G1 GS D.
+
 func call string, list argument, goal -> list sealed-goal.
 call Tac Args G GS :-
   set-goal-arguments Args G (seal G) (seal G1),
-  coq.ltac.call-ltac1 Tac G1 GS.
+  coq.ltac.call-ltac1 Tac G1 GS ok.
+
+func simple.call string, list argument, goal -> list goal, diagnostic.
+simple.call Tac Args G GS D :-
+  set-goal-arguments Args G (seal G) (seal G1),
+  coq.ltac.call-simple-ltac1 Tac G1 GS D.
 
 :index(_ _ 1)
 func set-goal-arguments list argument, goal, sealed-goal -> sealed-goal.
@@ -61,25 +83,47 @@ try _ G [G].
 
 %:index (_ 1) % TODO
 :external
-pred all i:tactic, i:list sealed-goal, o:list sealed-goal.
+pred all tactic, list sealed-goal -> list sealed-goal.
+all T [G|Gs] O :- T G O1, all T Gs O2, std.append O1 O2 O.
+all _ [] [].
+
+pred thenl list tactic, sealed-goal -> list sealed-goal.
+thenl [] G [G].
+thenl [T|Ts] G GS :- T G NG, all (thenl Ts) NG GS.
+
+pred repeat tactic, sealed-goal -> list sealed-goal.
+repeat T G GS :- T G GS1, all (repeat T) GS1 GS.
+repeat _ G [G].
+
+pred repeat! tactic, sealed-goal -> list sealed-goal.
+repeat! T G GS :- T G GS1, !, all (repeat! T) GS1 GS.
+repeat! _ G [G].
+
+pred or list tactic, sealed-goal -> list sealed-goal.
+or TL G GS :- std.exists TL (t\ t G GS).
+
+namespace simple {
+
+func all func-simple-tactic, list goal -> list goal.
 all T [G|Gs] O :- T G O1, all T Gs O2, std.append O1 O2 O.
 all _ [] [].
 
-pred thenl i:list tactic, i:sealed-goal, o:list sealed-goal.
+pred thenl list simple-tactic, goal -> list goal.
 thenl [] G [G].
 thenl [T|Ts] G GS :- T G NG, all (thenl Ts) NG GS.
 
-pred repeat i:tactic, i:sealed-goal, o:list sealed-goal.
+pred repeat simple-tactic, goal -> list goal.
 repeat T G GS :- T G GS1, all (repeat T) GS1 GS.
 repeat _ G [G].
 
-pred repeat! i:tactic, i:sealed-goal, o:list sealed-goal.
-repeat! T G GS :- T G GS1, !, all (repeat T) GS1 GS.
+func repeat! simple-tactic, goal -> list goal.
+repeat! T G GS :- T G GS1, !, all (repeat! T) GS1 GS.
 repeat! _ G [G].
 
-pred or i:list tactic, i:sealed-goal, o:list sealed-goal.
+pred or list simple-tactic, goal -> list goal.
 or TL G GS :- std.exists TL (t\ t G GS).
 
+}
 % :index (_ 1) TODO
 :external :index(_ 1)
 func open func-open-tactic, sealed-goal -> list sealed-goal.
diff --git a/examples/tutorial_coq_elpi_tactic.v b/examples/tutorial_coq_elpi_tactic.v
index 175d21bd9..e43bf0910 100644
--- a/examples/tutorial_coq_elpi_tactic.v
+++ b/examples/tutorial_coq_elpi_tactic.v
@@ -280,7 +280,7 @@ Ltac helper_split2 n t := fail n || apply t.
 Elpi Tactic split2.
 Elpi Accumulate lp:{{
   solve (goal _ _ {{ _ /\ _ }} _ _ as G) GL :-
-    coq.ltac.call "helper_split2" [int 0, trm {{ conj }}] G GL.
+    coq.ltac.call "helper_split2" [int 0, trm {{ conj }}] G GL ok.
   solve _ _ :-
     coq.ltac.fail _ "not a conjunction".
 }}.
diff --git a/rocq-elpi.opam b/rocq-elpi.opam
index bda1741bf..96bffb036 100644
--- a/rocq-elpi.opam
+++ b/rocq-elpi.opam
@@ -17,7 +17,7 @@ bug-reports: "https://github.com/LPCIC/coq-elpi/issues"
 depends: [
   "dune" {>= "3.13"}
   "ocaml" {>= "4.10.0"}
-  "elpi" {>= "3.3.0" & < "3.5.0~"}
+  "elpi" {>= "3.6.0" & < "3.7.0~"}
   "rocq-core" {>= "9.0+rc1" & < "9.2~" | = "dev"}
   "ppx_optcomp"
   "ocaml-lsp-server" {with-dev-setup}
diff --git a/src/rocq_elpi_HOAS.ml b/src/rocq_elpi_HOAS.ml
index abf531914..06c9a59de 100644
--- a/src/rocq_elpi_HOAS.ml
+++ b/src/rocq_elpi_HOAS.ml
@@ -436,7 +436,7 @@ let make_options ~hoas_holes ~local ~warn ~depr ~primitive ~failsafe ~ppwidth
     redflags; no_tc; algunivs; }
 let make_warn = UserWarn.make_warn
 
-type 'a coq_context = {
+type 'a conv_context = {
   section : Names.Id.t list;
   section_len : int;
   proof : EConstr.named_context;
@@ -449,8 +449,9 @@ type 'a coq_context = {
   db2rel : int Int.Map.t;
   names : Id.Set.t;
   options : options;
+  hyps : E.hyp list;
 }
-let upcast (x : [> `Options ] coq_context) : full coq_context = (x :> full coq_context)
+let upcast (x : [> `Options ] conv_context) : full conv_context = (x :> full conv_context)
 
 let pr_coq_ctx { env; db2name; db2rel } sigma =
   let open Pp in
@@ -471,7 +472,7 @@ let spropc   = E.Constants.declare_global_symbol "sprop"
 let typc   = E.Constants.declare_global_symbol "typ"
 
 
-let sort : (Sorts.t, _ coq_context, API.Data.constraints) API.ContextualConversion.t =
+let sort : (Sorts.t, _ conv_context, API.Data.constraints) API.ContextualConversion.t =
   let open API.ContextualConversion in
   {
   ty = API.Conversion.TyName "sort";
@@ -1286,7 +1287,7 @@ let get_options ~depth hyps state =
     | E.CData d -> CD.to_string d
     | _ -> assert false in
   let options =
-    E.of_hyps hyps |> CList.map_filter (fun { E.hdepth = depth; E.hsrc = t } ->
+    hyps |> CList.map_filter (fun { E.hdepth = depth; E.hsrc = t } ->
     match E.look ~depth t with
     | E.App(c,name,[p]) when c == get_optionc && is_string ~depth name ->
         Some (get_string ~depth name, (p,depth))
@@ -1409,7 +1410,7 @@ let get_options ~depth hyps state =
     make_options ~hoas_holes ~local ~warn ~depr ~primitive ~failsafe ~ppwidth
       ~pp ~pplevel ~using ~inline ~uinstance ~universe_decl ~reversible ~keepunivs
       ~redflags ~no_tc ~algunivs
-let mk_coq_context ~options state =
+let empty_conv_context ~options state =
   let env = get_global_env state in
   let section = section_ids env in
   {
@@ -1425,9 +1426,10 @@ let mk_coq_context ~options state =
     names = Environ.named_context env |> Context.Named.to_vars;
     env;
     options;
+    hyps = [];
   }
 
-let push_coq_ctx_proof i e coq_ctx =
+let push_coq_ctx_proof i (e,h) coq_ctx =
   assert(coq_ctx.local = []);
   let id = Context.Named.Declaration.get_id e in
  {
@@ -1438,6 +1440,7 @@ let push_coq_ctx_proof i e coq_ctx =
   db2name = Int.Map.add i id coq_ctx.db2name;
   name2db = Names.Id.Map.add id i coq_ctx.name2db;
   names = Id.Set.add id coq_ctx.names;
+  hyps = h :: coq_ctx.hyps;
 }
 
 let push_coq_ctx_local i e coq_ctx =
@@ -1451,17 +1454,18 @@ let push_coq_ctx_local i e coq_ctx =
 }
 
 (* Not sure this is sufficient, eg we don't restrict evars, but elpi shuld... *)
-let restrict_coq_context live_db state { proof; proof_len; local; name2db; env; options;  } =
+let restrict_conv_context live_db state { proof; proof_len; local; name2db; env; options; hyps } =
   let named_ctx =
-    mk_coq_context ~options state |> List.fold_right (fun e ctx ->
+    empty_conv_context ~options state |> List.fold_right2 (fun e h ctx ->
       let id = Context.Named.Declaration.get_id e in
       let db = Names.Id.Map.find id name2db in
       if List.mem db live_db
-      then push_coq_ctx_proof db e ctx
-      else ctx) proof in
+      then
+        push_coq_ctx_proof db (e,h) ctx
+      else ctx) proof hyps in
 
   debug Pp.(fun () ->
-      str "restrict_coq_context: named: " ++
+      str "restrict_conv_context: named: " ++
       Printer.pr_named_context_of named_ctx.env (get_sigma state));
 
   let subst_rel_decl env k s = function
@@ -1479,11 +1483,11 @@ let restrict_coq_context live_db state { proof; proof_len; local; name2db; env;
   (named_ctx,[]) |> List.fold_right (fun (db,e) (ctx,s) ->
 
       debug Pp.(fun () ->
-          str"restrict_coq_context: cur rel ctx: " ++
+          str"restrict_conv_context: cur rel ctx: " ++
           Printer.pr_rel_context_of ctx.env (get_sigma state) ++ fnl() ++
-          str"restrict_coq_context: cur subst: " ++
+          str"restrict_conv_context: cur subst: " ++
           prlist_with_sep spc (Printer.pr_econstr_env ctx.env (get_sigma state)) s ++ fnl() ++
-          str"restrict_coq_context: looking at " ++
+          str"restrict_conv_context: looking at " ++
           Names.Name.print (Context.Rel.Declaration.get_name e)
           ++ str"(dbl " ++ int db ++ str")");
 
@@ -1506,7 +1510,6 @@ let info_of_evar ~env ~sigma ~section k =
 (*  <---- depth ---->                          *)
 (*  proof_ctx |- pis \ t                       *)
 (* ******************************************* *)
-type hyp = { ctx_entry : E.term; depth : int }
 
 let declc = E.Constants.declare_global_symbol "decl"
 let defc = E.Constants.declare_global_symbol "def"
@@ -1631,50 +1634,49 @@ let rec constr2lp coq_ctx ~calldepth ~depth state t =
 and under_coq2elpi_ctx ~calldepth state ctx ?(mk_ctx_item=fun decl -> mk_pi_arrow decl) kont =
   let open Context.Named.Declaration in
   let gls = ref [] in
-  let rec aux i ~depth coq_ctx hyps state = function
-    | [] -> state, coq_ctx, hyps
+  let rec aux i ~depth coq_ctx state = function
+    | [] -> state, coq_ctx
     | LocalAssum (Context.{binder_name=coq_name}, ty) as e :: rest ->
         let name = Name coq_name in
         let state, ty, gls_ty = constr2lp coq_ctx ~calldepth ~depth:(depth+1) state ty in
         gls := gls_ty @ !gls;
-        let hyp = mk_decl ~depth name ~ty in
-        let hyps = { ctx_entry = hyp ; depth = depth + 1 } :: hyps in
-        let coq_ctx = push_coq_ctx_proof depth e coq_ctx in
-        aux (succ i) ~depth:(depth+1) coq_ctx hyps state rest
+        let hsrc = mk_decl ~depth name ~ty in
+        let hyp = { E.hsrc ; hdepth = depth + 1 } in
+        let coq_ctx = push_coq_ctx_proof depth (e,hyp) coq_ctx in
+        aux (succ i) ~depth:(depth+1) coq_ctx state rest
       | LocalDef (Context.{binder_name=coq_name},bo,ty) as e :: rest ->
         let name = Name coq_name in
         let state, ty, gls_ty = constr2lp coq_ctx ~calldepth ~depth:(depth+1) state ty in
         let state, bo, gls_bo = constr2lp coq_ctx ~calldepth ~depth:(depth+1) state bo in
         gls := gls_ty @ gls_bo @ !gls;
-        let hyp = mk_def ~depth name ~bo ~ty in
-        let hyps = { ctx_entry = hyp ; depth = depth + 1 } :: hyps in
-        let coq_ctx = push_coq_ctx_proof depth e coq_ctx in
-        aux (succ i) ~depth:(depth+1) coq_ctx hyps state rest
+        let hsrc = mk_def ~depth name ~bo ~ty in
+        let hyp = { E.hsrc ; hdepth = depth + 1 } in
+        let coq_ctx = push_coq_ctx_proof depth (e,hyp) coq_ctx in
+        aux (succ i) ~depth:(depth+1) coq_ctx state rest
   in
-  let state, coq_ctx, hyps =
-      let state, coq_ctx, hyps =
-        aux 0 ~depth:calldepth (mk_coq_context ~options:(default_options ()) state) [] state (List.rev ctx) in
-      state, coq_ctx, hyps in
-  let state, t, gls_t = kont coq_ctx hyps ~depth:(calldepth + List.length hyps) state in
+  let state, coq_ctx =
+    aux 0 ~depth:calldepth (empty_conv_context ~options:(default_options ()) state) state (List.rev ctx) in
+  let state, t, gls_t = kont coq_ctx ~depth:(calldepth + List.length coq_ctx.hyps) state in
   gls := gls_t @ !gls;
-  let t = List.fold_left (fun rest hyp -> mk_ctx_item hyp.ctx_entry rest) t hyps in
+  let t = List.fold_left (fun rest hyp -> mk_ctx_item hyp.E.hsrc rest) t coq_ctx.hyps in
   state, t, !gls
   
-and in_elpi_evar_concl evar_concl ~raw_uvar elpi_evk coq_ctx hyps ~calldepth ~depth state =
+and in_elpi_evar_concl evar_concl ~raw_uvar elpi_evk coq_ctx ~calldepth ~depth state =
   let state, evar_concl, gls_evar_concl = constr2lp coq_ctx ~calldepth ~depth state evar_concl in
   let args = CList.init coq_ctx.proof_len (fun i -> E.mkConst @@ i + calldepth) in
   debug Pp.(fun () -> str"in_elpi_evar_concl: moving Ctx down to" ++ int depth);
-  let hyps = List.map (fun { ctx_entry; depth = from } ->
-    U.move ~from ~to_:depth ctx_entry) hyps in
-  state, U.list_to_lp_list hyps,
+  let hyps = List.map (fun { E.hsrc = ctx_entry; hdepth = from } ->
+    U.move ~from ~to_:depth ctx_entry) coq_ctx.hyps
+    |> U.list_to_lp_list in
+  state, hyps,
   (E.mkUnifVar raw_uvar ~args state),
   (E.mkUnifVar elpi_evk ~args state),
   evar_concl, gls_evar_concl
 
 and in_elpi_evar_info ~calldepth ~env ~sigma ctx ~raw_ev:elpi_revk elpi_evk evar_concl state =
-  under_coq2elpi_ctx ~mk_ctx_item:(fun _ -> mk_pi) ~calldepth state ctx (fun coq_ctx hyps ~depth state ->
+  under_coq2elpi_ctx ~mk_ctx_item:(fun _ -> mk_pi) ~calldepth state ctx (fun coq_ctx ~depth state ->
     let state, hyps, raw_ev, ev, ty, gls =
-      in_elpi_evar_concl evar_concl ~raw_uvar:elpi_revk elpi_evk coq_ctx hyps
+      in_elpi_evar_concl evar_concl ~raw_uvar:elpi_revk elpi_evk coq_ctx
         ~calldepth ~depth state in
     state, E.mkApp declare_evc hyps [raw_ev; ty; ev], gls)
 
@@ -1868,14 +1870,14 @@ let find_evar var csts =
     | _ -> None) 
 
 let preprocess_context visible context =
-  let select_ctx_entries visible { E.hdepth = depth; E.hsrc = t } =
+  let select_ctx_entries visible ({ E.hdepth = depth; E.hsrc = t } as h) =
     let isVisibleConst t = match E.look ~depth t with E.Const i -> visible i | _ -> false in
     let destConst t = match E.look ~depth t with E.Const x -> x | _ -> assert false in
     match E.look ~depth t with
     | E.App(c,v,[name;ty]) when c == declc && isVisibleConst v ->
-       Some (destConst v, depth, `Decl(name,ty))
+       Some (destConst v, depth, h, `Decl(name,ty))
     | E.App(c,v,[name;ty;bo]) when c == defc && isVisibleConst v ->
-       Some (destConst v, depth, `Def (name,ty,bo))
+       Some (destConst v, depth, h, `Def (name,ty,bo))
     | _ ->
       debug Pp.(fun () ->
           str "skip entry" ++
@@ -1884,11 +1886,11 @@ let preprocess_context visible context =
   in
   let ctx_hyps = CList.map_filter (select_ctx_entries visible) context in
   let dbl2ctx =
-    List.fold_right (fun (i,d,e) m ->
+    List.fold_right (fun (i,d,t,e) m ->
       if Int.Map.mem i m
       then err Pp.(str "Duplicate context entry for " ++
                   str(pp2string (P.term d) (E.mkConst i)))
-      else Int.Map.add i (d,e) m)
+      else Int.Map.add i (d,t,e) m)
     ctx_hyps Int.Map.empty in
   dbl2ctx
 
@@ -2034,11 +2036,11 @@ let rec of_elpi_ctx ~calldepth syntactic_constraints depth dbl2ctx state initial
   in
   let rec build_ctx_entry coq_ctx state gls = function
     | [] -> state, coq_ctx, List.(concat (rev gls))
-    | (i,id,d,e) :: rest ->
+    | (i,id,d,h,e) :: rest ->
       debug Pp.(fun () -> str "<<< context entry for DBL "++ int i ++ str" at depth" ++ int d);
       let state, e, gl1 = of_elpi_ctx_entry id i coq_ctx ~depth:d e state in
       debug Pp.(fun () -> str "<<< context entry for DBL "++ int i ++ str" at depth" ++ int d);
-      let coq_ctx = push_coq_ctx_proof i e coq_ctx in
+      let coq_ctx = push_coq_ctx_proof i (e,h) coq_ctx in
       build_ctx_entry coq_ctx state (gl1 :: gls) rest
   in
   (* we go from the bottom (most recent addition) to the top in order to
@@ -2049,10 +2051,10 @@ let rec of_elpi_ctx ~calldepth syntactic_constraints depth dbl2ctx state initial
       if not (Int.Map.mem i dbl2ctx)
       then ctx_entries_names names (i - 1)
       else
-        let d, e = Int.Map.find i dbl2ctx in
+        let d, t, e = Int.Map.find i dbl2ctx in
         let id = of_elpi_ctx_entry_name i names ~depth:d e in
         let names = Id.Set.add (Context.binder_name id) names in
-        (i,id,d,e) :: ctx_entries_names names (i - 1)
+        (i,id,d,t,e) :: ctx_entries_names names (i - 1)
   in
     ctx_entries_names Id.Set.empty (depth-1) |>
     List.rev |> (* we need to readback the context from top to bottom *)
@@ -2323,7 +2325,7 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals
 
 (* Evar info out of thin air: the user wrote an X that was never encountered by
    type checking (of) hence we craft a tower ?1 : ?2 : Type and link X with ?1 *)
-and create_evar_unknown ~calldepth syntactic_constraints (coq_ctx : 'a coq_context) ~args_in_coq_ctx ~depth ~on_ty state elpi_evk orig =
+and create_evar_unknown ~calldepth syntactic_constraints (coq_ctx : 'a conv_context) ~args_in_coq_ctx ~depth ~on_ty state elpi_evk orig =
   debug Pp.(fun () ->
       str"lp2term: evar: create_unknown: whole ctx:" ++
       Printer.pr_named_context_of coq_ctx.env (get_sigma state) ++ str" ; "++
@@ -2332,7 +2334,7 @@ and create_evar_unknown ~calldepth syntactic_constraints (coq_ctx : 'a coq_conte
       str"lp2term: evar: create_unknown: visible ctx:" ++
       str (pp2string (P.list (P.term depth) " ") (List.map E.mkBound args_in_coq_ctx)));
 
-  let env = (restrict_coq_context args_in_coq_ctx state coq_ctx).env in
+  let env = (restrict_conv_context args_in_coq_ctx state coq_ctx).env in
 
   debug Pp.(fun () ->
       str"lp2term: evar: create_unknown: restricted ctx:" ++
@@ -2366,7 +2368,8 @@ and create_evar_unknown ~calldepth syntactic_constraints (coq_ctx : 'a coq_conte
 (* Evar info read back from a constraint (contains the context and the type) *)
 and declare_evar_of_constraint ~calldepth elpi_revkc elpi_evkc syntactic_constraints ctx (depth_concl,concl) state options =
   let state, coq_ctx, gl1 =
-    of_elpi_ctx ~calldepth syntactic_constraints depth_concl ctx state (mk_coq_context ~options state) in
+    of_elpi_ctx ~calldepth syntactic_constraints depth_concl ctx state
+      (empty_conv_context ~options state) in
   let state, ty, gl2 = lp2constr ~calldepth syntactic_constraints coq_ctx ~depth:depth_concl state concl in
   let state, k = S.update_return engine state (fun ({ sigma } as e) ->
     let sigma, t = Evarutil.new_evar~typeclass_candidate:false ~naming:(Namegen.IntroFresh (Names.Id.of_string "elpi_evar")) coq_ctx.env sigma ty in
@@ -2459,17 +2462,17 @@ let sealed_goal2lp ~depth ~args ~in_elpi_tac_arg ~base state k =
   let env = get_global_env state in
   let sigma = get_sigma state in
   let state, elpi_goal_evar, elpi_raw_goal_evar, evar_decls = in_elpi_evar ~calldepth k state in
-  let evar_concl, goal_ctx, goal_env =
+  let evar_concl, goal_ctx, _goal_env =
     info_of_evar ~env ~sigma ~section:(section_ids env) k in
   let state, g, gls =
     under_coq2elpi_ctx ~calldepth state goal_ctx
       ~mk_ctx_item:(fun _ t -> E.mkApp nablac (E.mkLam t) [])
-      (fun coq_ctx hyps ~depth state ->
+      (fun coq_ctx ~depth state ->
             let state, args, gls_args = API.Utils.map_acc (in_elpi_tac_arg ~base ~depth ?calldepth:(Some calldepth) coq_ctx [] sigma) state args in
             let args = List.flatten args in
             let state, hyps, raw_ev, ev, goal_ty, gls =
               in_elpi_evar_concl evar_concl ~raw_uvar:elpi_raw_goal_evar elpi_goal_evar
-                coq_ctx hyps ~calldepth ~depth state in
+                coq_ctx ~calldepth ~depth state in
           state, E.mkApp sealc (in_elpi_goal state ~args ~hyps ~raw_ev ~ty:goal_ty ~ev) [], gls_args @ gls) in
   state, g, evar_decls @ gls
 
@@ -2514,7 +2517,7 @@ let customtac2query sigma goals loc text ~depth:calldepth ~base state =
       info_of_evar ~env ~sigma ~section:(section_ids env) goal in
     let state, query, gls =
       under_coq2elpi_ctx ~calldepth state goal_ctx
-      (fun coq_ctx hyps ~depth state ->
+      (fun coq_ctx ~depth state ->
           let q = API.Quotation.elpi ~language:API.Quotation.elpi_language state loc text in
           let _amap, q = API.RawQuery.term_to_raw_term state base ~depth q in
           state, q, []) in
@@ -2638,7 +2641,7 @@ let elpi_solution_to_coq_solution ~eta_contract_solution ~calldepth syntactic_co
        let spilled_solution = ref (EConstr.mkProp) in
        let eta_reduced = ref false in
        let state, _, gls = under_coq2elpi_ctx ~calldepth:0 state ctx ~mk_ctx_item:(fun _ x -> x) 
-         (fun coq_ctx hyps ~depth state ->
+         (fun coq_ctx ~depth state ->
            debug Pp.(fun () ->
                str"solution for "++ Evar.print k ++ str" in ctx=" ++ cut () ++
                Printer.pr_named_context_of coq_ctx.env (get_sigma state) ++ cut () ++
@@ -2795,7 +2798,7 @@ let set_current_sigma ~depth state sigma =
           debug Pp.(fun () ->
               str"set_current_sigma: preparing assignment for " ++ str (pp2string (P.term depth) assigned) ++
               str" under context " ++ Printer.pr_named_context env sigma (EConstr.Unsafe.to_named_context ctx));
-          let state, t, dec = under_coq2elpi_ctx ~mk_ctx_item:(fun _ -> E.mkLam) ~calldepth:depth state ctx (fun coq_ctx hyps ~depth:new_ctx_depth state ->
+          let state, t, dec = under_coq2elpi_ctx ~mk_ctx_item:(fun _ -> E.mkLam) ~calldepth:depth state ctx (fun coq_ctx ~depth:new_ctx_depth state ->
             constr2lp coq_ctx ~calldepth:depth ~depth:new_ctx_depth state c) in
           let assignment = API.Conversion.Unify(assigned, t) in
           debug Pp.(fun () ->
@@ -3402,7 +3405,7 @@ let under_coq2elpi_relctx ~calldepth state (ctx : 'a ctx_entry list) ~coq_ctx ~m
         let state, ty, gls_ty = constr2lp coq_ctx ~calldepth ~depth state typ in
         gls := gls_ty @ !gls;
         let hyp = mk_decl ~depth name ~ty in
-        let hyps = { ctx_entry = hyp ; depth = depth } :: hyps in
+        let hyps = { E.hsrc = hyp ; hdepth = depth } :: hyps in
         let e = Context.Rel.Declaration.LocalAssum (annotR name, typ) in
         let coq_ctx = push_coq_ctx_local depth e coq_ctx in
         let state, rest = aux ~depth:(depth+1) coq_ctx hyps state rest in
@@ -3853,13 +3856,14 @@ let merge_universe_context state uctx =
 (* ****************************** API ********************************** *)
 
 module CtxReadbackCache = Ephemeron.K1.Make(struct
-  type t = API.Data.hyp list
+  type t = E.hyps
   let equal = (==)
   let hash = Hashtbl.hash
 end)
 let ctx_cache_lp2c = CtxReadbackCache.create 1
 
 let get_current_env_sigma ~depth hyps constraints state =
+  let hyps = E.of_hyps hyps in
   let state, _, changed, gl1 = elpi_solution_to_coq_solution ~eta_contract_solution:true ~calldepth:depth constraints state in
   if changed then CtxReadbackCache.reset ctx_cache_lp2c;
   let state, coq_ctx, gl2 =
@@ -3867,12 +3871,12 @@ let get_current_env_sigma ~depth hyps constraints state =
     | (c,e,d) when d == depth && e == Global.env () -> state, c, []
     | _ ->
       of_elpi_ctx ~calldepth:depth constraints depth
-        (preprocess_context (fun _ -> true) (E.of_hyps hyps))
-        state (mk_coq_context ~options:(get_options ~depth hyps state) state)
+        (preprocess_context (fun _ -> true) hyps)
+        state (empty_conv_context ~options:(get_options ~depth hyps state) state)
     | exception Not_found -> 
         of_elpi_ctx ~calldepth:depth constraints depth
-          (preprocess_context (fun _ -> true) (E.of_hyps hyps))
-          state (mk_coq_context ~options:(get_options ~depth hyps state) state)
+          (preprocess_context (fun _ -> true) hyps)
+          state (empty_conv_context ~options:(get_options ~depth hyps state) state)
   in
   CtxReadbackCache.reset ctx_cache_lp2c;
   CtxReadbackCache.add ctx_cache_lp2c hyps (coq_ctx,Global.env (),depth);
@@ -3880,8 +3884,9 @@ let get_current_env_sigma ~depth hyps constraints state =
 ;;
 
 let get_global_env_current_sigma ~depth hyps constraints state =
+  let hyps = E.of_hyps hyps in
   let state, _, changed, gls = elpi_solution_to_coq_solution ~eta_contract_solution:true ~calldepth:depth constraints state in
-  let coq_ctx = mk_coq_context ~options:(get_options ~depth hyps state) state in
+  let coq_ctx = empty_conv_context ~options:(get_options ~depth hyps state) state in
   let coq_ctx = { coq_ctx with env = Environ.set_universes (Evd.universes (get_sigma state)) coq_ctx.env } in
   state, coq_ctx, get_sigma state, gls
 ;;
@@ -3899,10 +3904,33 @@ let rec lp2goal ~depth hyps syntactic_constraints state t =
     let state, coq_ctx, gl2 =
       of_elpi_ctx ~calldepth:depth syntactic_constraints depth
         (preprocess_context (fun x -> Int.Set.mem x visible_set)
-          (U.lp_list_to_list ~depth ctx |> List.map (fun hsrc -> { E.hdepth = depth; E.hsrc })))
+          (U.lp_list_to_list ~depth ctx |>
+            List.map (fun hsrc -> { E.hdepth = depth; E.hsrc })))
         state
-        (mk_coq_context ~options:(get_options ~depth hyps state) state) in
-    state, coq_ctx, k, args, gl1@gl2
+        (empty_conv_context ~options:(get_options ~depth hyps state) state) in
+    state, (ctx, coq_ctx, k, args), gl1@gl2
+
+let goal2lp ~depth syntactic_constraints state (_ctx,coq_ctx,k) = (* TODO: reuse _ctx in in_elpi_evar_concl *)
+  let calldepth = depth in
+  let env = get_global_env state in
+  let sigma = get_sigma state in
+  let state, elpi_goal_evar, elpi_raw_goal_evar, evar_decls =
+    in_elpi_evar ~calldepth k state in
+  let evar_concl, goal_ctx, _goal_env =
+    info_of_evar ~env ~sigma ~section:(section_ids env) k in
+
+  let same_ctx sigma c1 c2 =
+    let eq_named_declaration =
+      Context.Named.Declaration.equal (EConstr.ERelevance.equal sigma) (EConstr.eq_constr sigma) in
+    CList.equal eq_named_declaration c1 c2 in
+  
+  if same_ctx sigma coq_ctx.proof goal_ctx then
+    let state, hyps, raw_ev, ev, goal_ty, gls =
+      in_elpi_evar_concl evar_concl ~raw_uvar:elpi_raw_goal_evar elpi_goal_evar
+        coq_ctx ~calldepth ~depth state in
+    Result.Ok (state, in_elpi_goal state ~args:[] ~hyps ~raw_ev ~ty:goal_ty ~ev, evar_decls@gls)
+  else
+    Result.Error goal_ctx
 
 let constr2lp ~depth ?(calldepth=depth) coq_ctx _constraints state t =
   constr2lp coq_ctx ~calldepth ~depth state t
diff --git a/src/rocq_elpi_HOAS.mli b/src/rocq_elpi_HOAS.mli
index d5050dbd9..7dbe6510a 100644
--- a/src/rocq_elpi_HOAS.mli
+++ b/src/rocq_elpi_HOAS.mli
@@ -60,7 +60,7 @@ type options = {
   algunivs : bool option;
 }
 
-type 'a coq_context = {
+type 'a conv_context = {
   (* Elpi representation of the context *)
   section : Names.Id.t list;
   section_len : int;
@@ -80,41 +80,44 @@ type 'a coq_context = {
 
   (* Options (get-option context entries) *)
   options : options;
+
+  (* the origin (when read from elpi) *)
+  hyps : hyps;
 }
-val mk_coq_context : options:options -> State.t -> empty coq_context
-val get_options : depth:int -> Data.hyps -> State.t -> options
+val empty_conv_context : options:options -> State.t -> empty conv_context
+val get_options : depth:int -> hyps -> State.t -> options
 val default_options : unit -> options
-val upcast : [> `Options ] coq_context -> full coq_context
+val upcast : [> `Options ] conv_context -> full conv_context
 
 val get_current_env_sigma : depth:int ->
-  Data.hyps -> constraints -> State.t -> State.t * full coq_context * Evd.evar_map * Conversion.extra_goals
+  Data.hyps -> constraints -> State.t -> State.t * full conv_context * Evd.evar_map * Conversion.extra_goals
 val set_current_sigma : depth:int -> State.t -> Evd.evar_map -> State.t * Conversion.extra_goals
 val get_global_env_current_sigma : depth:int ->
-  Data.hyps -> constraints -> State.t -> State.t * empty coq_context * Evd.evar_map * Conversion.extra_goals
+  Data.hyps -> constraints -> State.t -> State.t * empty conv_context * Evd.evar_map * Conversion.extra_goals
 
 (* HOAS of terms *)
 val constr2lp :
-  depth:int -> ?calldepth:int -> full coq_context -> constraints -> State.t ->
+  depth:int -> ?calldepth:int -> full conv_context -> constraints -> State.t ->
   EConstr.t -> State.t * term * Conversion.extra_goals
 
 (* readback: adds to the evar map universes and evars in the term *)
 val lp2constr :
-  depth:int -> full coq_context -> constraints -> State.t -> 
+  depth:int -> full conv_context -> constraints -> State.t -> 
   term -> State.t * EConstr.t * Conversion.extra_goals
 
 (* variants in the global context *)
-val constr2lp_closed : depth:int -> ?calldepth:int -> empty coq_context -> constraints -> State.t ->
+val constr2lp_closed : depth:int -> ?calldepth:int -> empty conv_context -> constraints -> State.t ->
   EConstr.t -> State.t * term * Conversion.extra_goals
-val lp2constr_closed :  depth:int -> empty coq_context -> constraints -> State.t ->
+val lp2constr_closed :  depth:int -> empty conv_context -> constraints -> State.t ->
   term -> State.t * EConstr.t * Conversion.extra_goals
-val constr2lp_closed_ground : depth:int -> ?calldepth:int -> empty coq_context -> constraints -> State.t ->
+val constr2lp_closed_ground : depth:int -> ?calldepth:int -> empty conv_context -> constraints -> State.t ->
   EConstr.t -> State.t * term * Conversion.extra_goals
-val lp2constr_closed_ground :  depth:int -> empty coq_context -> constraints -> State.t ->
+val lp2constr_closed_ground :  depth:int -> empty conv_context -> constraints -> State.t ->
   term -> State.t * EConstr.t * Conversion.extra_goals
 
 (* another variant, to call the pretyper *)
 val lp2skeleton :
-  depth:int -> full coq_context -> constraints -> State.t ->
+  depth:int -> full conv_context -> constraints -> State.t ->
   term -> State.t * Glob_term.glob_constr * Conversion.extra_goals
 
 type coercion_status = Regular | Off | Reversible
@@ -122,11 +125,11 @@ type record_field_spec = { name : Name.t; is_coercion : coercion_status; is_cano
 
 [%%if coq = "9.0"]
 val lp2inductive_entry :
-  depth:int -> empty coq_context -> constraints -> State.t -> term ->
+  depth:int -> empty conv_context -> constraints -> State.t -> term ->
   State.t * (DeclareInd.default_dep_elim list * Entries.mutual_inductive_entry * Univ.ContextSet.t * UnivNames.universe_binders * (bool * record_field_spec list) option * DeclareInd.one_inductive_impls list) * Conversion.extra_goals
 [%%else]
 val lp2inductive_entry :
-  depth:int -> empty coq_context -> constraints -> State.t -> term ->
+  depth:int -> empty conv_context -> constraints -> State.t -> term ->
   State.t * (DeclareInd.default_dep_elim list * Entries.mutual_inductive_entry * Univ.ContextSet.t * UState.named_universes_entry * (bool * record_field_spec list) option * DeclareInd.one_inductive_impls list) * Conversion.extra_goals
 [%%endif]
 
@@ -137,15 +140,15 @@ val lp2record_field_spec : record_field_spec -> Name.t * Record.Data.projection_
 [%%endif]
 
 val inductive_decl2lp :
-  depth:int -> empty coq_context -> constraints -> State.t -> (Names.MutInd.t * UVars.Instance.t * (Declarations.mutual_inductive_body * Declarations.one_inductive_body) * (Glob_term.binding_kind list * Glob_term.binding_kind list list)) ->
+  depth:int -> empty conv_context -> constraints -> State.t -> (Names.MutInd.t * UVars.Instance.t * (Declarations.mutual_inductive_body * Declarations.one_inductive_body) * (Glob_term.binding_kind list * Glob_term.binding_kind list list)) ->
     State.t * term * Conversion.extra_goals
 
 val inductive_entry2lp :
-  depth:int -> empty coq_context -> constraints -> State.t -> loose_udecl:bool -> ComInductive.Mind_decl.t ->
+  depth:int -> empty conv_context -> constraints -> State.t -> loose_udecl:bool -> ComInductive.Mind_decl.t ->
     State.t * term * Conversion.extra_goals
 
 val record_entry2lp :
-  depth:int -> empty coq_context -> constraints -> State.t -> loose_udecl:bool ->Record.Record_decl.t ->
+  depth:int -> empty conv_context -> constraints -> State.t -> loose_udecl:bool ->Record.Record_decl.t ->
     State.t * term * Conversion.extra_goals
   
 val in_elpi_id : Names.Name.t -> term
@@ -160,8 +163,12 @@ val in_elpi_indtdecl_inductive : State.t -> Declarations.recursivity_kind -> Nam
 val in_elpi_indtdecl_constructor : Names.Name.t -> term -> term
 
 val sealed_goal2lp : depth:int -> State.t -> Evar.t -> State.t * term * Conversion.extra_goals
-val lp2goal : depth:int -> Data.hyps -> constraints -> State.t -> term -> 
-  State.t * full coq_context * Evar.t * term list * Conversion.extra_goals
+val lp2goal : depth:int -> hyps -> constraints -> State.t -> term -> 
+  State.t * (term * full conv_context * Evar.t * term list) * Conversion.extra_goals
+
+(* checks the evar context is the same as the one in input *)
+val goal2lp : depth:int -> constraints -> State.t -> term * full conv_context * Evar.t -> 
+  (State.t * term * Conversion.extra_goals,EConstr.named_context) Result.t
 
 (* *** Low level API to reuse parts of the embedding *********************** *)
 val unspec2opt : 'a Elpi.Builtin.unspec -> 'a option
@@ -171,7 +178,7 @@ val in_elpi_gr : depth:int -> State.t -> Names.GlobRef.t -> term
 val in_elpi_poly_gr : depth:int -> State.t -> Names.GlobRef.t -> term -> term
 val in_elpi_poly_gr_instance : depth:int -> State.t -> Names.GlobRef.t -> UVars.Instance.t -> term
 val in_elpi_flex_sort : term -> term
-val in_elpi_sort : depth:int -> 'a coq_context -> constraints -> state -> Sorts.t -> state * term * Conversion.extra_goals
+val in_elpi_sort : depth:int -> 'a conv_context -> constraints -> state -> Sorts.t -> state * term * Conversion.extra_goals
 val in_elpi_prod : Name.t -> term -> term -> term
 val in_elpi_lam : Name.t -> term -> term -> term
 val in_elpi_let : Name.t -> term -> term -> term -> term
@@ -214,7 +221,7 @@ val gref : Names.GlobRef.t Conversion.t
 val inductive : inductive Conversion.t
 val constructor : constructor Conversion.t
 val constant : global_constant Conversion.t
-val sort : (Sorts.t,'a coq_context,constraints) ContextualConversion.t
+val sort : (Sorts.t,'a conv_context,constraints) ContextualConversion.t
 val global_constant_of_globref : Names.GlobRef.t -> global_constant
 val abbreviation : Globnames.abbreviation Conversion.t
 val implicit_kind : Glob_term.binding_kind Conversion.t
@@ -335,11 +342,9 @@ 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
 
-type hyp = { ctx_entry : term; depth : int }
-
 val solvegoals2query :
   Evd.evar_map -> Evar.t list -> Elpi.API.Ast.Loc.t -> main:'a list ->
-  in_elpi_tac_arg:(base:'base -> depth:int -> ?calldepth:int -> 'b coq_context -> hyp list -> Evd.evar_map -> State.t -> 'a -> State.t * term list * Conversion.extra_goals) ->
+  in_elpi_tac_arg:(base:'base -> depth:int -> ?calldepth:int -> 'b conv_context -> hyp list -> Evd.evar_map -> State.t -> 'a -> State.t * term list * Conversion.extra_goals) ->
   depth:int -> base:'base -> State.t -> State.t * term * Conversion.extra_goals
 val txtgoals2query :
   Evd.evar_map -> Evar.t list -> Elpi.API.Ast.Loc.t -> main:string ->
diff --git a/src/rocq_elpi_arg_HOAS.mli b/src/rocq_elpi_arg_HOAS.mli
index 58d253e80..8469a19fa 100644
--- a/src/rocq_elpi_arg_HOAS.mli
+++ b/src/rocq_elpi_arg_HOAS.mli
@@ -114,8 +114,8 @@ val in_elpi_tac :
   base: Elpi.API.Compile.program ->
   depth:int ->
   ?calldepth:int -> 
-  Rocq_elpi_HOAS.full Rocq_elpi_HOAS.coq_context ->
-  Rocq_elpi_HOAS.hyp list ->
+  Rocq_elpi_HOAS.full Rocq_elpi_HOAS.conv_context ->
+  hyps ->
   Evd.evar_map ->
   Elpi.API.State.t ->
   Tac.top ->
@@ -125,8 +125,8 @@ val in_elpi_tac :
 val in_elpi_tac_econstr :
   base:unit ->
   depth:int -> ?calldepth:int -> 
-  Rocq_elpi_HOAS.full Rocq_elpi_HOAS.coq_context ->
-  Rocq_elpi_HOAS.hyp list ->
+  Rocq_elpi_HOAS.full Rocq_elpi_HOAS.conv_context ->
+  hyps ->
   Evd.evar_map ->
   Elpi.API.State.t ->
   EConstr.t ->
@@ -138,7 +138,7 @@ val in_elpi_cmd :
   depth:int ->
   base:Elpi.API.Compile.program ->
   ?calldepth:int -> 
-  Rocq_elpi_HOAS.empty Rocq_elpi_HOAS.coq_context ->
+  Rocq_elpi_HOAS.empty Rocq_elpi_HOAS.conv_context ->
   Elpi.API.State.t ->
   raw:bool ->
   Cmd.top ->
@@ -153,7 +153,7 @@ type coq_arg = Cint of int | Cstr of string | Ctrm of EConstr.t | CLtac1 of Geni
 
 val in_coq_arg :
   depth:int ->
-  Rocq_elpi_HOAS.full Rocq_elpi_HOAS.coq_context ->
+  Rocq_elpi_HOAS.full Rocq_elpi_HOAS.conv_context ->
   Elpi.API.Data.constraints ->
   Elpi.API.State.t ->
   term ->
diff --git a/src/rocq_elpi_builtins.ml b/src/rocq_elpi_builtins.ml
index 949f13ad6..a977a66dd 100644
--- a/src/rocq_elpi_builtins.ml
+++ b/src/rocq_elpi_builtins.ml
@@ -17,6 +17,22 @@ module B = struct
   let ioargC_flex = API.BuiltInPredicate.ioargC_flex
   (* let ioarg_flex = API.BuiltInPredicate.ioarg_flex *)
   let ioarg_poly s = { ioarg_any with API.Conversion.ty = API.Conversion.TyName s }
+
+  let listC (d : ('a,'h,'cst) CConv.t) =
+    let embed ~depth h cst s l =
+      let s, l, eg = API.Utils.map_acc (d.CConv.embed ~depth h cst ) s l in
+      s, API.Utils.list_to_lp_list l, eg in
+    let readback ~depth h cst s t =
+      API.Utils.map_acc (d.CConv.readback ~depth h cst) s
+        (API.Utils.lp_list_to_list ~depth t)
+    in
+    let pp fmt l =
+      Format.fprintf fmt "[%a]" (API.RawPp.list d.CConv.pp ~boxed:true "; ") l in
+    { CConv.embed; readback;
+      ty = TyApp ("list",d.CConv.ty,[]);
+      pp;
+      pp_doc = (fun fmt () -> ()) }
+
 end
 module Pred = API.BuiltInPredicate
 module U = API.Utils
@@ -132,6 +148,12 @@ let pr_named_decl_flagged flags env sigma d =
 let empty_extern_env () = Constrextern.empty_extern_env ~flags:(PrintingFlags.Extern.current())
 [%%endif]
 
+let pr_named_context_of options env sigma =
+  let make_decl_list env d pps =
+    with_pp_options options.pp (fun flags -> pr_named_decl_flagged flags env sigma d) :: pps in
+  let psl = List.rev (Environ.fold_named_context make_decl_list env ~init:[]) in
+  Pp.(v 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl))
+
 let with_no_tc ~no_tc f sigma =
   if no_tc then
     let typeclass_evars = Evd.get_typeclass_evars sigma in
@@ -258,7 +280,7 @@ let failsafe_term = {
   embed = constr2lp;
 }
 
-let proof_context : (full coq_context, API.Data.constraints) CConv.ctx_readback =
+let proof_context : (full conv_context, API.Data.constraints) CConv.ctx_readback =
   fun ~depth hyps constraints state ->
     let state, proof_context, _, gls = get_current_env_sigma ~depth hyps constraints state in
     state, proof_context, constraints, gls
@@ -270,7 +292,7 @@ let closed_term = {
   readback = lp2constr_closed;
   embed = constr2lp_closed
 }
-let global : (empty coq_context, API.Data.constraints) CConv.ctx_readback =
+let global : (empty conv_context, API.Data.constraints) CConv.ctx_readback =
   fun ~depth hyps constraints state ->
     let state, proof_context, _, gls = get_global_env_current_sigma ~depth hyps constraints state in
     state, proof_context, constraints, gls
@@ -302,18 +324,47 @@ let sealed_goal = {
   readback = (fun ~depth _ _ -> assert false);
 }
 
-let goal : ( (Rocq_elpi_HOAS.full Rocq_elpi_HOAS.coq_context * Evar.t * Rocq_elpi_arg_HOAS.coq_arg list) , API.Data.hyps, API.Data.constraints) CConv.t = {
+type goal = E.term option * E.term * Rocq_elpi_HOAS.full Rocq_elpi_HOAS.conv_context * Evar.t * Rocq_elpi_arg_HOAS.coq_arg list
+
+let goal_readback ~depth hyps csts state g =
+    let state, (ctx,coq_ctx, k, raw_args), gls1 = Rocq_elpi_HOAS.lp2goal ~depth hyps csts state g in
+    let state, args, gls2 = U.map_acc (Rocq_elpi_arg_HOAS.in_coq_arg ~depth coq_ctx csts) state raw_args in
+    state, (None,ctx,coq_ctx,k,args), gls1 @ gls2
+
+let goal_embed ~depth _ csts state (tac,ctx,coq_ctx,ev,args) =
+    assert(args=[]);
+    match Rocq_elpi_HOAS.goal2lp ~depth csts state (ctx,coq_ctx,ev) with
+    | Result.Ok (st, r, gl) -> st,r,gl
+    | Result.Error env ->
+        let old_env = coq_ctx.env in
+        let msg =
+          Pp.string_of_ppcmds
+          Pp.(strbrk "coq.ltac.call-simple-ltac1: The tactic "
+            ++ Option.cata (fun tac -> str (pp2string (API.RawPp.term depth) tac)) (mt ()) tac
+            ++ strbrk " generates a subgoal that lives in a different context."
+            ++ fnl () ++ str "Input context:" ++ fnl ()
+            ++ pr_named_context_of coq_ctx.options old_env (get_sigma state)
+            ++ fnl () ++ str "Output context:" ++ fnl ()
+            ++ pr_named_context_of coq_ctx.options (Environ.reset_with_named_context (EConstr.val_of_named_context env) old_env) (get_sigma state))
+        in
+        U.type_error msg
+
+let goal : ( goal , API.Data.hyps, API.Data.constraints) CConv.t = {
   CConv.ty = Conv.TyName "goal";
   pp_doc = (fun fmt () -> ());
   pp = (fun fmt _ -> Format.fprintf fmt "TODO");
-  embed = (fun ~depth _ _ _ _ -> assert false);
-  readback = (fun ~depth hyps csts state g ->
-    let state, ctx, k, raw_args, gls1 = Rocq_elpi_HOAS.lp2goal ~depth hyps csts state g in
-    let state, args, gls2 = U.map_acc (Rocq_elpi_arg_HOAS.in_coq_arg ~depth ctx csts) state raw_args in
-    state, (ctx,k,args), gls1 @ gls2);
+  embed = goal_embed;
+  readback = (fun ~depth hyps csts st g -> goal_readback ~depth (E.of_hyps hyps) csts st g)
+}
+let goal' : ( goal , Rocq_elpi_HOAS.full Rocq_elpi_HOAS.conv_context , API.Data.constraints) CConv.t = {
+  CConv.ty = Conv.TyName "goal";
+  pp_doc = (fun fmt () -> ());
+  pp = (fun fmt _ -> Format.fprintf fmt "TODO");
+  embed = (fun ~depth hyps csts state x -> goal_embed ~depth hyps.hyps csts state x);
+  readback = (fun ~depth hyps csts state g -> goal_readback ~depth hyps.hyps csts state g);
 }
 
-let tactic_arg : (Rocq_elpi_arg_HOAS.coq_arg, Rocq_elpi_HOAS.full Rocq_elpi_HOAS.coq_context, API.Data.constraints) CConv.t = {
+let tactic_arg : (Rocq_elpi_arg_HOAS.coq_arg, Rocq_elpi_HOAS.full Rocq_elpi_HOAS.conv_context, API.Data.constraints) CConv.t = {
   CConv.ty = Conv.TyName "argument";
   pp_doc = (fun fmt () -> ());
   pp = (fun fmt _ -> Format.fprintf fmt "TODO");
@@ -321,6 +372,42 @@ let tactic_arg : (Rocq_elpi_arg_HOAS.coq_arg, Rocq_elpi_HOAS.full Rocq_elpi_HOAS
   readback = Rocq_elpi_arg_HOAS.in_coq_arg;
 }
 
+let goals_of_term state proof_context proof =
+  let env = proof_context.env in
+  let sigma = get_sigma state in
+  let evars_of_term c =
+    let rec evrec env (acc_set,acc_rev_l as acc) c =
+      match EConstr.kind sigma c with
+      | Constr.Evar (n, l) ->
+        if Evar.Set.mem n acc_set then
+          acc
+        else
+          let acc = Evar.Set.add n acc_set, n :: acc_rev_l in
+          SList.Skip.fold (evrec env) acc l
+      | Constr.Proj (_, _, c) ->
+        let t = Retyping.get_type_of env sigma c in
+        let acc = evrec env acc t in
+        evrec env acc c
+      | _ -> Termops.fold_constr_with_full_binders env sigma EConstr.push_rel evrec env acc c
+    in
+    let _, rev_l = evrec env (Evar.Set.empty, []) c in
+    List.rev rev_l in
+  let subgoals = evars_of_term proof in
+  let free_evars =
+    let cache = Evarutil.create_undefined_evars_cache () in
+    let map ev =
+      let EvarInfo evi = Evd.find sigma ev in
+      let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in
+      (ev, fevs)
+    in
+    List.map map subgoals in
+  let shelved_subgoals, subgoals =
+    CList.partition
+      (fun g ->
+          CList.exists (fun (tgt, lazy evs) -> not (Evar.equal g tgt) && Evar.Set.mem g evs) free_evars)
+      subgoals in
+  shelved_subgoals, subgoals
+
 let id = Rocq_elpi_builtins_synterp.id
 
 let flag name = { (B.unspec bool) with Conv.ty = Conv.TyName name }
@@ -1477,7 +1564,7 @@ let coq_print pp msg_f =
   (fun args ~depth _hyps _constraints state ->
      let pp = pp ~depth in
      msg_f Pp.(str (pp2string (P.list ~boxed:true pp " ") args));
-     state, ())
+     state, (), [])
 
 (*****************************************************************************)
 (*****************************************************************************)
@@ -1561,32 +1648,60 @@ let apply_proof ~name ~poly env tac pf =
   pv
 [%%endif]
 
+let apply_ltac1 ~depth tac tac_args =
+  let open Ltac_plugin in
+  let tac =
+    match E.look ~depth tac with
+    | E.CData s when API.RawOpaqueData.is_string s ->
+        let tac_name = API.RawOpaqueData.to_string s in
+        let tac_name =
+          let q = Libnames.qualid_of_string tac_name in
+          try Tacenv.locate_tactic q
+          with Not_found ->
+            match Tacenv.locate_extended_all_tactic q with
+            | [x] -> x
+            | _::_::_ -> err Pp.(str"Ltac1 tactic " ++ str tac_name ++ str" is ambiguous, qualify the name")
+            | [] -> err Pp.(str"Ltac1 tactic " ++ str tac_name ++ str" not found") in
+        let tacref = Locus.ArgArg (Loc.tag @@ tac_name) in
+        let tacexpr = Tacexpr.(CAst.make @@ TacArg (TacCall (CAst.make @@ (tacref, [])))) in
+        Tacinterp.Value.of_closure (Tacinterp.default_ist ()) tacexpr
+    | E.CData t when Rocq_elpi_arg_HOAS.is_ltac_tactic t ->
+        Rocq_elpi_arg_HOAS.to_ltac_tactic t
+    | _ -> U.type_error ("coq.ltac.call-ltac1: string or ltac1-tactic are expected as the tactic to call")
+  in
+  Tacinterp.Value.apply tac tac_args
+
+exception TacticFails of Exninfo.iexn
+
 let call_tactic ~depth state ~no_tc proof_context goal tactic =
   let sigma = get_sigma state in
-  let sigma, subgoals =
-    let open Proofview in let open Notations in
-    let focused_tac =
-      Unsafe.tclSETGOALS [with_empty_state goal] <*> tactic in
-    with_no_tc ~no_tc (fun sigma ->
-      let _, pv = init sigma [] in
-      let pv =
-        let vernac_state = Vernacstate.freeze_full_state () in
-        try
-          let rc = apply_proof ~name:(Id.of_string "elpi") ~poly:default_polyflags proof_context.env focused_tac pv in
-          let pstate = Vernacstate.Stm.pstate (Vernacstate.freeze_full_state ()) in
-          let vernac_state = Vernacstate.Stm.set_pstate vernac_state pstate in
-          Vernacstate.unfreeze_full_state vernac_state;
-          rc
-        with e when CErrors.noncritical e ->
-          Vernacstate.unfreeze_full_state vernac_state;
-          raise Pred.No_clause
-      in
-      let subgoals, sigma = proofview pv in
-      sigma, subgoals)
-  sigma in
-  Declare.Internal.export_side_effects (Evd.eval_side_effects sigma);
-  let state, assignments = set_current_sigma ~depth state sigma in
-  state, subgoals, assignments
+  try 
+    let sigma, subgoals =
+      let open Proofview in let open Notations in
+      let focused_tac =
+        Unsafe.tclSETGOALS [with_empty_state goal] <*> tactic in
+      with_no_tc ~no_tc (fun sigma ->
+        let _, pv = init sigma [] in
+        let pv =
+          let vernac_state = Vernacstate.freeze_full_state () in
+          try
+            let rc = apply_proof ~name:(Id.of_string "elpi") ~poly:default_polyflags proof_context.env focused_tac pv in
+            let pstate = Vernacstate.Stm.pstate (Vernacstate.freeze_full_state ()) in
+            let vernac_state = Vernacstate.Stm.set_pstate vernac_state pstate in
+            Vernacstate.unfreeze_full_state vernac_state;
+            rc
+          with e when CErrors.noncritical e ->
+            let e = Exninfo.capture e in
+            Vernacstate.unfreeze_full_state vernac_state;
+            raise (TacticFails e)
+        in
+        let subgoals, sigma = proofview pv in
+        sigma, subgoals)
+    sigma in
+    Declare.Internal.export_side_effects (Evd.eval_side_effects sigma);
+    let state, assignments = set_current_sigma ~depth state sigma in
+    Result.Ok (state, subgoals, assignments)
+  with TacticFails e -> Result.Error e
 
 [%%if coq = "9.0"]
 let section_close_section x =
@@ -1651,7 +1766,7 @@ let coq_misc_builtins =
          | _ -> None, x :: args
      in
      warning ?loc (pp2string (P.list ~boxed:true pp " ") args);
-     state, ()
+     state, (), []
      )),
   DocAbove);
 
@@ -1686,7 +1801,7 @@ line option|}))),
      in
      let txt = pp2string (P.list ~boxed:true pp " ") args in
      if coq_warning_cache category_name name loc txt then warning ?loc txt;
-     state, ())),
+     state, (), [])),
   DocAbove);
 
   MLCode(Pred("coq.error",
@@ -2178,7 +2293,7 @@ Supported attributes:
     Out(list constant, "ConstantsRepresentingVariables",
     Read(unit_ctx, "lists all the section variables, i.e. the global objects that are marked as to be abstracted at the end of the enclosing sections")),
   (fun _ ~depth _ _ state ->
-     let { section } = mk_coq_context ~options:(default_options ()) state in
+     let { section } = empty_conv_context ~options:(default_options ()) state in
      !: (section |> List.map (fun x -> Variable x)) )),
   DocAbove);
 
@@ -2673,15 +2788,15 @@ denote the same x as before.|};
     InOut(B.ioarg constant, "Compatibility constant",
     Out(int, "Index",
     Read(global, "Relates a primitive projection to its compatibility constant. Index is set to the constructor argument extracted by the projection (starting from 0).")))),
-    (fun p c _ ~depth coq_context _ _ ->
+    (fun p c _ ~depth conv_context _ _ ->
       match p, c with
       | _, Data (Variable c) -> raise No_clause
       | Data p, Data (Constant c) ->
-          if Environ.QConstant.equal coq_context.env (Projection.constant p) c then ?: None +? None +! Names.Projection.(arg p + npars p) else raise No_clause
+          if Environ.QConstant.equal conv_context.env (Projection.constant p) c then ?: None +? None +! Names.Projection.(arg p + npars p) else raise No_clause
       | NoData, NoData -> U.type_error "coq.env.primitive-projection?: got no input data"
       | Data p, NoData -> ?: None +! (Constant (Projection.constant p)) +! Names.Projection.(arg p + npars p)
       | NoData, Data (Constant c) ->
-          (match Environ.constant_opt_value_in coq_context.env (UVars.in_punivs c) with
+          (match Environ.constant_opt_value_in conv_context.env (UVars.in_punivs c) with
           | None -> raise No_clause
           | Some p ->
             let rec get_proj c =
@@ -3018,14 +3133,14 @@ declared as cumulative.|};
     InOut(B.ioarg projection,"P",
     InOut(B.ioarg projection,"PU",
     Read(global, "Relates a primitive projection P to its unfolded version PU. PU is still a primitive projection, but it is displayed as a match and some Ltac code can see that."))),
-    (fun p q ~depth:_ coq_context _ _ ->
+    (fun p q ~depth:_ conv_context _ _ ->
       let test_folded = function Data x -> if Projection.unfolded x then raise No_clause | _ -> () in
       let test_unfolded = function Data x -> if not (Projection.unfolded x) then raise No_clause | _ -> () in
       test_folded p;
       test_unfolded q;
       match p, q with
       | Data p, Data q ->
-          if Environ.QProjection.Repr.equal coq_context.env (Projection.repr p) (Projection.repr q) then ?: None +? None else raise No_clause
+          if Environ.QProjection.Repr.equal conv_context.env (Projection.repr p) (Projection.repr q) then ?: None +? None else raise No_clause
       | NoData, NoData -> U.type_error "coq.projection.unfolded: got no input data"
       | Data p, NoData -> ?: None +! Projection.(make (repr p) true)
       | NoData, Data q -> !: Projection.(make (repr q) false) +? None
@@ -4032,7 +4147,7 @@ coq.reduction.lazy.whd_all X Y :-
      ltac_fail_err level msg)),
   DocAbove);
 
-  MLCode(Pred("coq.ltac.collect-goals",
+  MLCode(Pred("coq.ltac.collect-sealed-goals",
     CIn(failsafe_term, "T",
     Out(list sealed_goal, "Goals",
     Out(list sealed_goal, "ShelvedGoals",
@@ -4045,39 +4160,7 @@ The order of Goals is given by the traversal order of EConstr.fold (a
 fold_left over the terms, letin body comes before the type).
 |})))),
     (fun proof _ shelved ~depth proof_context constraints state ->
-      let env = proof_context.env in
-      let sigma = get_sigma state in
-      let evars_of_term c =
-        let rec evrec env (acc_set,acc_rev_l as acc) c =
-          match EConstr.kind sigma c with
-          | Constr.Evar (n, l) ->
-            if Evar.Set.mem n acc_set then
-              acc
-            else
-              let acc = Evar.Set.add n acc_set, n :: acc_rev_l in
-              SList.Skip.fold (evrec env) acc l
-          | Constr.Proj (_, _, c) ->
-            let t = Retyping.get_type_of env sigma c in
-            let acc = evrec env acc t in
-            evrec env acc c
-          | _ -> Termops.fold_constr_with_full_binders env sigma EConstr.push_rel evrec env acc c
-        in
-        let _, rev_l = evrec env (Evar.Set.empty, []) c in
-        List.rev rev_l in
-      let subgoals = evars_of_term proof in
-      let free_evars =
-        let cache = Evarutil.create_undefined_evars_cache () in
-        let map ev =
-          let EvarInfo evi = Evd.find sigma ev in
-          let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in
-          (ev, fevs)
-        in
-        List.map map subgoals in
-      let shelved_subgoals, subgoals =
-        CList.partition
-          (fun g ->
-             CList.exists (fun (tgt, lazy evs) -> not (Evar.equal g tgt) && Evar.Set.mem g evs) free_evars)
-          subgoals in
+      let shelved_subgoals, subgoals = goals_of_term state proof_context proof in
       let shelved =
         match shelved with
         | Keep -> Some shelved_subgoals
@@ -4086,12 +4169,39 @@ fold_left over the terms, letin body comes before the type).
     )),
     DocAbove);
 
+  LPCode {|
+func coq.ltac.collect-goals term -> list sealed-goal, list sealed-goal.
+coq.ltac.collect-goals T GA GB :- coq.ltac.collect-sealed-goals T GA GB.
+|};
+
+  MLCode(Pred("coq.ltac.collect-simple-goals",
+    CIn(failsafe_term, "T",
+    COut(B.listC goal', "Goals",
+    Out(list sealed_goal, "ShelvedGoals",
+    Full(proof_context, {|Like coq.ltac.collect-sealed-goals turns the holes in T into
+Goals but fails if the goals do not live in the current proof context.
+|})))),
+    (fun proof _ shelved ~depth proof_context constraints state ->
+      let shelved_subgoals, subgoals = goals_of_term state proof_context proof in
+      let shelved =
+        match shelved with
+        | Keep -> Some shelved_subgoals
+        | Discard -> None in
+      (* TODO FIXME *)
+      let ctx = U.list_to_lp_list [] in
+      let subgoals = List.map (fun ev -> Some (API.RawOpaqueData.of_string "collect-simple-goals"),ctx,proof_context,ev,[]) subgoals in
+      state, !: subgoals +? shelved, []
+    )),
+    DocAbove);
+
+
   MLCode(Pred("coq.ltac.call-mltac",
     In(B.string, "PluginName",
     In(B.string, "BlockName",
     In(B.int, "BlockIndex",
     CIn(goal, "G",
     Out(list sealed_goal,"GL",
+    InOut(B.ioarg B.diagnostic, "Diagnostic",
     Full(raw_ctx, {|Calls OCaml code bound via TACTIC EXTEND. For example the
 OCaml code for lia looks like:
 
@@ -4108,9 +4218,11 @@ In order to call the code between curly braces one has to run
 Note that each TACTIC EXTEND block can have many entries and their numbering
 starts from 0. Also, each block has a name, "Lia" in this case.
     
+When the diagnostic is (error Msg), then GL is not set.
+
 Supported attributes:
-- @no-tc! (default false, do not infer typeclasses)|})))))),
-    (fun plugin block index (proof_context,goal,tac_args) _ ~depth _ _ -> abstract__grab_global_env_keep_sigma "coq.ltac.call-mltac" (fun state ->
+- @no-tc! (default false, do not infer typeclasses)|}))))))),
+    (fun plugin block index (_,_,proof_context,goal,tac_args) _ diag ~depth _ _ -> abstract__grab_global_env_keep_sigma "coq.ltac.call-mltac" (fun state ->
       let no_tc = if proof_context.options.no_tc = Some true then true else false in
       let open Ltac_plugin in
 
@@ -4123,11 +4235,56 @@ Supported attributes:
          let tacname = Tacexpr.{ mltac_name  = { mltac_plugin  = plugin; mltac_tactic = block; }; mltac_index = index } in
          Tacenv.interp_ml_tactic tacname tac_args (Tacinterp.default_ist ()) in
 
-      let state, subgoals, assignments =
-        call_tactic ~depth state ~no_tc proof_context goal tactic in
+      match call_tactic ~depth state ~no_tc proof_context goal tactic with
+      | Result.Ok (state, subgoals, assignments) ->
+        (* universe constraints fixed by the code above*)
+        Univ.ContextSet.empty, state, !: subgoals +! B.mkOK, assignments
+      | Result.Error ie ->
+        match diag with
+        | Data B.OK -> raise No_clause (* optimization: don't print the error if caller wants OK *)
+        | _ ->
+          let error = string_of_ppcmds proof_context.options @@ CErrors.iprint_no_report ie in
+          Univ.ContextSet.empty, state, ?: None +! B.mkERROR error, []
+      ))),
+  DocAbove);
+
+  MLCode(Pred("coq.ltac.call-simple-mltac",
+    In(B.string, "PluginName",
+    In(B.string, "BlockName",
+    In(B.int, "BlockIndex",
+    CIn(goal, "G",
+    COut(B.listC goal,"GL",
+    InOut(B.ioarg B.diagnostic, "Diagnostic",
+    Full(raw_ctx, {|Like coq.ltac.call-mltac but Tac is not allowed to
+generate new goals GL in different contexts. For example "intro" does not
+obey this restriction.
+
+Supported attributes:
+- @no-tc! (default false, do not infer typeclasses)|}))))))),
+    (fun plugin block index (_,ctx,proof_context,goal,tac_args) _ diag ~depth _ _ -> abstract__grab_global_env_keep_sigma "coq.ltac.call-mltac" (fun state ->
+      let no_tc = if proof_context.options.no_tc = Some true then true else false in
+      let open Ltac_plugin in
 
-       (* universe constraints fixed by the code above*)
-       Univ.ContextSet.empty, state, !: subgoals, assignments
+       let tac_args = tac_args |> List.map (function
+         | Rocq_elpi_arg_HOAS.Ctrm t -> Tacinterp.Value.of_constr t
+         | Rocq_elpi_arg_HOAS.Cstr s -> Geninterp.(Val.inject (val_tag (Genarg.topwit Stdarg.wit_string))) s
+         | Rocq_elpi_arg_HOAS.Cint i -> Tacinterp.Value.of_int i
+         | Rocq_elpi_arg_HOAS.CLtac1 x -> Geninterp.(Val.inject (val_tag (Topwit Ltac_plugin.Tacarg.wit_tactic))) x) in
+       let tactic =
+         let tacname = Tacexpr.{ mltac_name  = { mltac_plugin  = plugin; mltac_tactic = block; }; mltac_index = index } in
+         Tacenv.interp_ml_tactic tacname tac_args (Tacinterp.default_ist ()) in
+
+      match call_tactic ~depth state ~no_tc proof_context goal tactic with
+      | Result.Ok (state, subgoals, assignments) ->
+        let subgoals = List.map (fun ev -> Some (API.RawOpaqueData.of_string (Format.asprintf "%s#%s(%d)" plugin block index)),ctx,proof_context,ev,[]) subgoals in
+        (* universe constraints fixed by the code above*)
+        Univ.ContextSet.empty, state, !: subgoals +! B.mkOK, assignments
+      | Result.Error ie ->
+        match diag with
+        | Data B.OK -> raise No_clause (* optimization: don't print the error if caller wants OK *)
+        | _ ->
+          let error = string_of_ppcmds proof_context.options @@ CErrors.iprint_no_report ie in
+          Univ.ContextSet.empty, state, ?: None +! B.mkERROR error, []
       ))),
   DocAbove);
 
@@ -4136,7 +4293,8 @@ Supported attributes:
     In(B.any, "Tac",
     CIn(goal, "G",
     Out(list sealed_goal,"GL",
-    Full(raw_ctx, {|Calls Ltac1 tactic Tac on goal G (passing the arguments of G, see coq.ltac.call for a handy wrapper).
+    VariadicInOut(raw_ctx,B.ioargC (CConv.(!>) B.diagnostic), {|Calls Ltac1 tactic Tac on goal G (passing the arguments of G, see coq.ltac.call for a handy wrapper).
+It accepts one diagnostic argument, defaults to ok if omitted.
 Tac can either be a string (the tactic name), or a value
 of type ltac1-tactic, see the tac argument constructor
 and the ltac_tactic:(...) syntax to pass arguments to
@@ -4146,9 +4304,12 @@ Caveat:
   "Ltac name := body", it cannot be a builtin one. For example
   "Ltac myapply x := apply x." lets one call apply by running
   coq.ltac.call-ltac1 "myapply" G GL.
+
+When the diagnostic is (error Msg), then GL is not set.
+
 Supported attributes:
 - @no-tc! (default false, do not infer typeclasses)|})))),
-    (fun tac (proof_context,goal,tac_args) _ ~depth _ _ -> abstract__grab_global_env_keep_sigma "coq.ltac.call-ltac1" (fun state ->
+    (fun tac (_,_,proof_context,goal,tac_args) _ diags ~depth _ _ -> abstract__grab_global_env_keep_sigma "coq.ltac.call-ltac1" (fun state ->
       let no_tc = if proof_context.options.no_tc = Some true then true else false in
       let open Ltac_plugin in
 
@@ -4157,33 +4318,56 @@ Supported attributes:
          | Rocq_elpi_arg_HOAS.Cstr s -> Geninterp.(Val.inject (val_tag (Genarg.topwit Stdarg.wit_string))) s
          | Rocq_elpi_arg_HOAS.Cint i -> Tacinterp.Value.of_int i
          | Rocq_elpi_arg_HOAS.CLtac1 x -> x) in
-       let tactic =
-         let tac =
-          match E.look ~depth tac with
-          | E.CData s when API.RawOpaqueData.is_string s ->
-              let tac_name = API.RawOpaqueData.to_string s in
-              let tac_name =
-                let q = Libnames.qualid_of_string tac_name in
-                try Tacenv.locate_tactic q
-                with Not_found ->
-                  match Tacenv.locate_extended_all_tactic q with
-                  | [x] -> x
-                  | _::_::_ -> err Pp.(str"Ltac1 tactic " ++ str tac_name ++ str" is ambiguous, qualify the name")
-                  | [] -> err Pp.(str"Ltac1 tactic " ++ str tac_name ++ str" not found") in
-              let tacref = Locus.ArgArg (Loc.tag @@ tac_name) in
-              let tacexpr = Tacexpr.(CAst.make @@ TacArg (TacCall (CAst.make @@ (tacref, [])))) in
-              Tacinterp.Value.of_closure (Tacinterp.default_ist ()) tacexpr
-          | E.CData t when Rocq_elpi_arg_HOAS.is_ltac_tactic t ->
-              Rocq_elpi_arg_HOAS.to_ltac_tactic t
-          | _ -> U.type_error ("coq.ltac.call-ltac1: string or ltac1-tactic are expected as the tactic to call")
-         in
-         Tacinterp.Value.apply tac tac_args in
+       let tactic = apply_ltac1 ~depth tac tac_args in
+
+      match call_tactic ~depth state ~no_tc proof_context goal tactic with
+      | Result.Ok (state, subgoals, assignments) ->
+        (* universe constraints fixed by the code above*)
+        Univ.ContextSet.empty, state, !: subgoals +! [Some B.mkOK], assignments
+      | Result.Error ie ->
+        match diags with
+        | [] -> raise No_clause (* optimization: don't print the error if caller wants OK *)
+        | _ :: _ :: _ -> U.type_error "coq.ltac.call-ltac1: too many arguments"
+        | [Data B.OK] -> raise No_clause (* optimization: don't print the error if caller wants OK *)
+        | _ ->
+          let error = string_of_ppcmds proof_context.options @@ CErrors.iprint_no_report ie in
+          Univ.ContextSet.empty, state, ?: None +! [Some(B.mkERROR error)], []
+      ))),
+  DocAbove);
+
+  MLCode(Pred("coq.ltac.call-simple-ltac1",
+    In(B.any, "Tac",
+    CIn(goal, "G",
+    COut(B.listC goal,"GL",
+    InOut(B.ioarg B.diagnostic, "Diagnostic",
+    Full(raw_ctx, {|Like coq.ltac.call-ltac1 but Tac is not allowed to
+generate new goals GL in different contexts. For example "intro" does not
+obey this restriction.
 
-      let state, subgoals, assignments =
-        call_tactic ~depth state ~no_tc proof_context goal tactic in
+Supported attributes:
+- @no-tc! (default false, do not infer typeclasses)|}))))),
+    (fun tac (_,ctx,proof_context,goal,tac_args) _ diag ~depth _ _ -> abstract__grab_global_env_keep_sigma "coq.ltac.call-simple-ltac1" (fun state ->
+      let no_tc = if proof_context.options.no_tc = Some true then true else false in
+      let open Ltac_plugin in
 
-       (* universe constraints fixed by the code above*)
-       Univ.ContextSet.empty, state, !: subgoals, assignments
+       let tac_args = tac_args |> List.map (function
+         | Rocq_elpi_arg_HOAS.Ctrm t -> Tacinterp.Value.of_constr t
+         | Rocq_elpi_arg_HOAS.Cstr s -> Geninterp.(Val.inject (val_tag (Genarg.topwit Stdarg.wit_string))) s
+         | Rocq_elpi_arg_HOAS.Cint i -> Tacinterp.Value.of_int i
+         | Rocq_elpi_arg_HOAS.CLtac1 x -> x) in
+       let tactic = apply_ltac1 ~depth tac tac_args in
+
+      match call_tactic ~depth state ~no_tc proof_context goal tactic with
+      | Result.Ok (state, subgoals, assignments) ->
+        let subgoals = List.map (fun ev -> Some tac,ctx,proof_context,ev,[]) subgoals in
+        (* universe constraints fixed by the code above*)
+        Univ.ContextSet.empty, state, !: subgoals +! B.mkOK, assignments
+      | Result.Error ie ->
+        match diag with
+        | Data B.OK -> raise No_clause (* optimization: don't print the error if caller wants OK *)
+        | _ ->
+          let error = string_of_ppcmds proof_context.options @@ CErrors.iprint_no_report ie in
+          Univ.ContextSet.empty, state, ?: None +! B.mkERROR error, []
       ))),
   DocAbove);
 
@@ -4196,7 +4380,7 @@ Supported attributes:
     hints), but for the ergonomy of a tactic it may help to know if an
     hypothesis name is already taken.
 |}))),
-  (fun id (proof_context,_,_) ~depth _ _ _ ->
+  (fun id (_,_,proof_context,_,_) ~depth _ _ _ ->
      if not @@ Id.Set.mem (Names.Id.of_string_soft id) proof_context.names then ()
      else raise No_clause)),
   DocAbove);
@@ -4383,12 +4567,12 @@ Supported attributes:
 - @ppmost! (default: false, prints most details)
 - @pplevel! (default: _, prints parentheses to reach that level, 200 = off)
 - @holes! (default: false, prints evars as _)|}))),
-  (fun (proof_context,evar,args) _ ~depth _ _ state ->
+  (fun (_,_,proof_context,evar,args) _ ~depth _ _ state ->
      let sigma = get_sigma state in
      let pr_named_context_of flags env sigma =
-      let make_decl_list env d pps = pr_named_decl_flagged flags env sigma d :: pps in
-      let psl = List.rev (Environ.fold_named_context make_decl_list env ~init:[]) in
-      Pp.(v 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl)) in
+        let make_decl_list env d pps = pr_named_decl_flagged flags env sigma d :: pps in
+        let psl = List.rev (Environ.fold_named_context make_decl_list env ~init:[]) in
+        Pp.(v 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl)) in
      let s = Pp.(repr @@ with_pp_options proof_context.options.pp (fun flags ->
         v 0 @@
         pr_named_context_of flags proof_context.env sigma ++ cut () ++
diff --git a/src/rocq_elpi_builtins.mli b/src/rocq_elpi_builtins.mli
index 1af5f5f45..ef015d6a1 100644
--- a/src/rocq_elpi_builtins.mli
+++ b/src/rocq_elpi_builtins.mli
@@ -23,4 +23,4 @@ val base : Compile.program option State.component
 
 val cache_tac_abbrev : code:qualified_name -> name:qualified_name ->unit
 
-val closed_term : (EConstr.t, Rocq_elpi_HOAS.empty Rocq_elpi_HOAS.coq_context, Data.constraints) ContextualConversion.t
+val closed_term : (EConstr.t, Rocq_elpi_HOAS.empty Rocq_elpi_HOAS.conv_context, Data.constraints) ContextualConversion.t
diff --git a/src/rocq_elpi_builtins_synterp.ml b/src/rocq_elpi_builtins_synterp.ml
index e8a4eb49f..eede687c1 100644
--- a/src/rocq_elpi_builtins_synterp.ml
+++ b/src/rocq_elpi_builtins_synterp.ml
@@ -34,7 +34,7 @@ type scope = ExecutionSite | CurrentModule | Library
 
 let options : (options, API.Data.constraints) CConv.ctx_readback =
   fun ~depth hyps constraints state ->
-    state, get_options ~depth hyps state, constraints, []
+    state, get_options ~depth (API.RawData.of_hyps hyps) state, constraints, []
 
 let scope = let open Conv in let open API.AlgebraicData in declare {
   ty = TyName "scope";
diff --git a/src/rocq_elpi_glob_quotation.ml b/src/rocq_elpi_glob_quotation.ml
index c4a777872..08e710712 100644
--- a/src/rocq_elpi_glob_quotation.ml
+++ b/src/rocq_elpi_glob_quotation.ml
@@ -185,7 +185,7 @@ let set_coq_ctx_hyps s (x,h) =
   set_glob_ctx s (glob_ctx_of_coq_ctx (upcast x))
 
 let under_ctx name ty bo ~k ~depth state =
-  let coq_ctx, hyps as orig_ctx = Option.default (upcast @@ mk_coq_context ~options:(default_options ()) state,[]) (get_ctx state) in
+  let coq_ctx, hyps as orig_ctx = Option.default (upcast @@ empty_conv_context ~options:(default_options ()) state,[]) (get_ctx state) in
   let orig_glob_ctx = S.get glob_ctx state in
   let state =
     let id =
@@ -199,7 +199,7 @@ let under_ctx name ty bo ~k ~depth state =
       match bo with
       | None -> state, mk_decl ~depth name ~ty
       | Some bo -> state, mk_def ~depth name ~bo ~ty in
-    let new_hyp = { ctx_entry; depth } in
+    let new_hyp = { E.hsrc = ctx_entry; hdepth = depth } in
     let state = set_coq_ctx_hyps state ({ coq_ctx with name2db }, new_hyp :: hyps) in
     let state = push_glob_ctx state id None in
     state in
@@ -616,7 +616,7 @@ let _ = API.Quotation.register_named_quotation ~name:"gref" ~descriptor:interp_q
    
 let gterm2lp ~loc ~base glob ~depth state =
   let t = gterm2lpast ~pattern:false ~language:coq state glob in
-  let coq_ctx, _ = Option.default (upcast @@ mk_coq_context ~options:(default_options ()) state,[]) (get_ctx state) in
+  let coq_ctx, _ = Option.default (upcast @@ empty_conv_context ~options:(default_options ()) state,[]) (get_ctx state) in
   let ctx = Names.Id.Map.fold (fun id i m ->
     API.Ast.Scope.Map.add (API.Ast.Name.from_string @@ Names.Id.to_string id,coq) i m
     ) coq_ctx.name2db API.Ast.Scope.Map.empty in
@@ -625,7 +625,7 @@ let gterm2lp ~loc ~base glob ~depth state =
 
 let runtime_gterm2lp ~loc ~base glob ~depth state =
   let t = gterm2lpast ~pattern:false ~language:coq state glob in
-  let coq_ctx, _ = Option.default (upcast @@ mk_coq_context ~options:(default_options ()) state,[]) (get_ctx state) in
+  let coq_ctx, _ = Option.default (upcast @@ empty_conv_context ~options:(default_options ()) state,[]) (get_ctx state) in
   let ctx = Names.Id.Map.fold (fun id i m ->
     API.Ast.Scope.Map.add (API.Ast.Name.from_string @@ Names.Id.to_string id,coq) i m
     ) coq_ctx.name2db API.Ast.Scope.Map.empty in
diff --git a/src/rocq_elpi_glob_quotation.mli b/src/rocq_elpi_glob_quotation.mli
index 9640baa3e..5ba0e87a7 100644
--- a/src/rocq_elpi_glob_quotation.mli
+++ b/src/rocq_elpi_glob_quotation.mli
@@ -9,7 +9,7 @@ open RawData
 val coq : Ast.Scope.language
   
 (* The context used to interpret Var("x") nodes in all the APIs below *)
-val set_coq_ctx_hyps : State.t -> [> `Options ] Rocq_elpi_HOAS.coq_context * Rocq_elpi_HOAS.hyp list -> State.t
+val set_coq_ctx_hyps : State.t -> [> `Options ] Rocq_elpi_HOAS.conv_context * hyps -> State.t
 
 val under_ctx :
   Names.Name.t -> term -> term option ->
diff --git a/src/rocq_elpi_vernacular.ml b/src/rocq_elpi_vernacular.ml
index ef1263fd2..debf43c25 100644
--- a/src/rocq_elpi_vernacular.ml
+++ b/src/rocq_elpi_vernacular.ml
@@ -553,7 +553,8 @@ module Interp = struct
       let query state =
         let depth = 0 in
         let state, args, gls = EU.map_acc
-          (Rocq_elpi_arg_HOAS.in_elpi_cmd ~loc ~depth ~base:program ~raw:raw_args Rocq_elpi_HOAS.(mk_coq_context ~options:(default_options ()) state))
+          (Rocq_elpi_arg_HOAS.in_elpi_cmd ~loc ~depth ~base:program ~raw:raw_args
+            Rocq_elpi_HOAS.(empty_conv_context ~options:(default_options ()) state))
           state args in
         let loc = Rocq_elpi_utils.of_coq_loc loc in
 
@@ -640,7 +641,8 @@ let run_program_open_proof ~loc name ~atts ~syndata args : Declare.Proof.t =
        let typ =
         try
           let t = API.Setup.StrMap.find "Statement" assignments in
-          let state, t, _ = Rocq_elpi_builtins.closed_term.readback ~depth:0 Rocq_elpi_HOAS.(mk_coq_context ~options:(default_options()) state) constraints state t in
+          let state, t, _ = Rocq_elpi_builtins.closed_term.readback ~depth:0
+            Rocq_elpi_HOAS.(empty_conv_context ~options:(default_options()) state) constraints state t in
           Some t
         with Not_found | Elpi.API.Conversion.TypeErr _ -> None in
        let data = relocate "Data" in
@@ -667,7 +669,8 @@ let run_program_close_proof ~loc name ~atts ~syndata args ~lemma =
     | Some(x,y,f) -> (fun ~target ~depth s -> f ~target ~depth |> Result.map (fun x -> s,x)), (Some(x,y)) in
   let p = Declare.Proof.get lemma |> Proof.partial_proof |> List.hd in (* all of them *)
   let proof ~target:_ ~depth state =
-    let state, p, _ = Rocq_elpi_builtins.closed_term.embed Rocq_elpi_HOAS.(mk_coq_context ~options:(default_options ()) state) Elpi.API.RawData.no_constraints ~depth state p in
+    let state, p, _ = Rocq_elpi_builtins.closed_term.embed
+      Rocq_elpi_HOAS.(empty_conv_context ~options:(default_options ()) state) Elpi.API.RawData.no_constraints ~depth state p in
     Ok(state, p) in
   let data ~target ~depth state = get_stash (Declare.Proof.get_name lemma) ~target ~depth |> Result.map (fun x -> state,x) in
   (run_program ~loc name ~main:main_end_proof ~atts ~syndata args [syn;proof;data]) |> (function
diff --git a/tests-stdlib/test_open_terms.v b/tests-stdlib/test_open_terms.v
index 15b41abef..d9e1e104a 100644
--- a/tests-stdlib/test_open_terms.v
+++ b/tests-stdlib/test_open_terms.v
@@ -264,7 +264,7 @@ solve (goal _ _ {{lp:X = lp:Y }} _ [Arg1, Arg2] as G) GL1 :-
   preserve_bound_variables X X1,
   refine {{@eq_trans _ lp:X1 lp:Y2 _ _ (eq_sym lp:P)}} G GL,
   if (GL = [Ng, Ng2])
-    (coq.ltac.open (coq.ltac.call "lazy_beta" []) Ng2 GL_aux,
+    (coq.ltac.open (g\gl\coq.ltac.call "lazy_beta" [] g gl ok) Ng2 GL_aux,
      GL1 = [Ng | GL_aux])
     (GL1 = GL).
   % refine {{eq_sym (@eq_trans lp:Y lp:Y2 lp:X lp:P (eq_sym _))}} G GL.
diff --git a/tests-stdlib/test_ring.v b/tests-stdlib/test_ring.v
index 3b8fb8149..36bc54c59 100644
--- a/tests-stdlib/test_ring.v
+++ b/tests-stdlib/test_ring.v
@@ -5,7 +5,7 @@ From Stdlib Require Import ZArith Lia.
 
 Elpi Tactic xlia.
 Elpi Accumulate lp:{{
-  solve G GL :- coq.ltac.call-mltac "rocq-runtime.plugins.micromega" "Lia" 0 G GL.
+  solve G GL :- coq.ltac.call-mltac "rocq-runtime.plugins.micromega" "Lia" 0 G GL ok.
 }}.
 Tactic Notation "mylia" :=
   Zify.zify; elpi xlia ltac_tactic:(zchecker).
@@ -24,7 +24,7 @@ Ltac xx rl :=
 
 Elpi Tactic test.
 Elpi Accumulate lp:{{
-  solve (goal C R T E []) GL :- coq.ltac.call-ltac1 "xx" (goal C R T E [trm {{ 0 + 0 }}]) GL.
+  solve (goal C R T E []) GL :- coq.ltac.call-ltac1 "xx" (goal C R T E [trm {{ 0 + 0 }}]) GL ok.
 }}.
 
 Goal forall f, 0 = f (0 + 0) :> Z.
diff --git a/tests/test_HOAS.v b/tests/test_HOAS.v
index e3c82f62c..6a81e7998 100644
--- a/tests/test_HOAS.v
+++ b/tests/test_HOAS.v
@@ -25,7 +25,7 @@ Elpi Tactic test2.
 Elpi Accumulate lp:{{
 
 solve (goal [decl T _ _ | _ ] _ _ _ _ as G) GS :-
-  coq.ltac.call "foobar" [trm T] G GS,
+  coq.ltac.call "foobar" [trm T] G GS ok,
   coq.say GS.
 
 }}.
diff --git a/tests/test_ltac.v b/tests/test_ltac.v
index 36d800576..7023950d4 100644
--- a/tests/test_ltac.v
+++ b/tests/test_ltac.v
@@ -40,7 +40,7 @@ Elpi Accumulate lp:{{
   main [] :-
     coq.elaborate-skeleton _ {{ True }} Bo ok,
     coq.ltac.collect-goals Bo [SealedGoal] [],
-    coq.ltac.open (coq.ltac.call "horror" []) SealedGoal [],
+    coq.ltac.open (g\gl\coq.ltac.call "horror" [] g gl ok) SealedGoal [],
     coq.locate "elpi_subproof" _,
     coq.env.add-const "it" Bo _ @transparent! C_.
 
@@ -97,3 +97,36 @@ Fail elpi barendregt True.
 elpi barendregt.
 elpi barendregt True.
 Abort.
+
+
+(*******************)
+
+Elpi Tactic simple.
+Elpi Accumulate lp:{{
+  solve G GL :-
+    coq.say G,
+    refine.simple-elaborate {{ conj _ _ }} G GL',
+    coq.say GL',
+    std.map GL' (x\r\r = seal x) GL. 
+  solve G GL :-
+    coq.say G,
+    refine.simple-elaborate {{ ex_intro _ (fun w => _) _ }} G GL',
+    coq.say GL',
+    std.map GL' (x\r\r = seal x) GL. 
+
+}}.
+
+Goal True -> False -> True /\ False.
+intros.
+elpi simple.
+assumption.
+assumption.
+Abort.
+
+Goal exists f : nat -> nat, forall y, y = f 1.
+intros.
+elpi simple.
+Unshelve.
+admit.
+Show.
+Abort.
\ No newline at end of file
diff --git a/tests/test_ltac3.v b/tests/test_ltac3.v
index c07b9d1a7..f8a23449d 100644
--- a/tests/test_ltac3.v
+++ b/tests/test_ltac3.v
@@ -10,7 +10,7 @@ Elpi Tactic fail_foo.
 Elpi Accumulate lp:{{
 
 solve (goal _ _ _ _ [_] as G) GS :-
-  coq.ltac.call "ltac_foo" [] G GS.
+  coq.ltac.call "ltac_foo" [] G GS ok.
 
 }}.
 
diff --git a/tests/test_tactic.v b/tests/test_tactic.v
index 7096e34aa..e52fa78dd 100644
--- a/tests/test_tactic.v
+++ b/tests/test_tactic.v
@@ -379,7 +379,7 @@ End Test.
 Elpi Tactic app.
 Elpi Accumulate lp:{{
   solve (goal C R T P [tac F, tac X]) GL :-
-    coq.ltac.call-ltac1 F (goal C R T P [tac X]) GL.
+    coq.ltac.call-ltac1 F (goal C R T P [tac X]) GL ok.
 }}.
 
 
@@ -428,4 +428,34 @@ Elpi Accumulate lp:{{
 Goal forall x: nat, x =x.
 Proof.
   elpi create_goal.
-Abort.
\ No newline at end of file
+Abort.
+
+
+(** test simple call *)
+
+Elpi Tactic simple_call.
+Elpi Accumulate lp:{{
+  solve (goal C R Ty E [str T] as G) [seal G'] :-
+    std.assert-ok! (coq.ltac.call-simple-ltac1 T (goal C R Ty E []) [G']) T.
+}}.
+
+Goal forall x y: nat, x = y.
+Proof.
+  intros.
+  elpi simple_call "symmetry".
+  match goal with |- y = x => idtac end.
+Abort.
+
+Ltac myintros := intros.
+Ltac myrefl := reflexivity.
+
+Goal forall x y: nat, x = y.
+Proof.
+  Fail elpi simple_call "myintros".
+Abort.
+
+Goal forall x y: nat, x = y.
+Proof.
+  intros.
+  Fail elpi simple_call "myrefl".
+Abort.
diff --git a/tests/test_vernacular2.v b/tests/test_vernacular2.v
index ea288ff2a..f41d68d23 100644
--- a/tests/test_vernacular2.v
+++ b/tests/test_vernacular2.v
@@ -20,7 +20,7 @@ Elpi Accumulate lp:{{
     std.assert-ok! (coq.elaborate-skeleton Lem _ ELem) "failed",
     std.assert-ok! (coq.typecheck {{ lp:Bo : lp:ELem }} _) "failed",
     coq.ltac.collect-goals Bo [SealedGoal] [],
-    coq.ltac.open (coq.ltac.call "ltac1_that_calls_elpi" []) SealedGoal [],
+    coq.ltac.open (g\gl\coq.ltac.call "ltac1_that_calls_elpi" [] g gl ok) SealedGoal [],
     % !tactic_mode should equal false here
     coq.env.add-const Name Bo ELem @transparent! C_,
   ].