diff --git a/Changelog.md b/Changelog.md
index 273d83c89..07a218cca 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,5 +1,20 @@
 # Changelog
 
+## [1.10.1] - 24-05-2021
+
+Requires Elpi 1.13.5 and Coq 8.13.
+
+### HOAS
+- Fix (reverse) the order of the context argument of `goal`. The head of
+  the list is the most recent hypothesis and in the last to be loaded (the
+  one with higher precedence) by implication when one writes `Ctx => ...`.
+- New `msolve` entry point for (possibly multi goal) tactics
+
+### API
+- Fix argument interpretation for `coq.ltac.call-ltac1`, the context is now the
+  one of the goal alone (and not the one of the goal plus the current one)
+- Rename `coq.ltac.then` to `coq.ltac.all`
+
 ## [1.10.0] - 21-05-2021
 
 Requires Elpi 1.13.5 and Coq 8.13.
diff --git a/apps/eltac/_CoqProject b/apps/eltac/_CoqProject
index a7b35380b..19fd8c53d 100644
--- a/apps/eltac/_CoqProject
+++ b/apps/eltac/_CoqProject
@@ -16,4 +16,5 @@ theories/discriminate.v
 theories/injection.v
 theories/case.v
 theories/generalize.v
+theories/cycle.v
 theories/tactics.v
diff --git a/apps/eltac/_CoqProject.test b/apps/eltac/_CoqProject.test
index 5543e3399..7a87bbf7f 100644
--- a/apps/eltac/_CoqProject.test
+++ b/apps/eltac/_CoqProject.test
@@ -18,5 +18,6 @@ tests/test_discriminate.v
 tests/test_injection.v
 tests/test_case.v
 tests/test_generalize.v
+tests/test_cycle.v
 
 examples/usage_eltac.v
diff --git a/apps/eltac/tests/test_cycle.v b/apps/eltac/tests/test_cycle.v
new file mode 100644
index 000000000..aeac91254
--- /dev/null
+++ b/apps/eltac/tests/test_cycle.v
@@ -0,0 +1,22 @@
+From elpi.apps Require Import eltac.cycle.
+
+Goal True /\ False /\ 1=1.
+split;[|split].
+all: eltac.cycle 1.
+admit.
+reflexivity.
+exact I.
+Abort.
+
+Goal True /\ False /\ 1=1.
+split;[|split].
+all: eltac.cycle -1.
+reflexivity.
+exact I.
+admit.
+Abort.
+
+Goal True /\ False /\ 1=1.
+split;[|split].
+Fail all: eltac.cycle 3.
+Abort.
\ No newline at end of file
diff --git a/apps/eltac/theories/clear.v b/apps/eltac/theories/clear.v
index 3cb09ff5c..83bd758c2 100644
--- a/apps/eltac/theories/clear.v
+++ b/apps/eltac/theories/clear.v
@@ -7,8 +7,8 @@ Elpi Accumulate lp:{{
   not-hyp X (def Y _ Ty Bo) Y :- not (occurs X Ty ; occurs X Bo), not (X = Y).
 
   solve (goal Ctx R T E [trm X]) [seal (goal Ctx R T E [])] :- name X, !, std.do! [
-    std.map-filter Ctx (not-hyp X) Visible,
-    prune E1 Visible,
+    std.map-filter Ctx (not-hyp X) VisibleRev,
+    prune E1 {std.rev VisibleRev}, % preserve the order
     std.assert-ok! (coq.typecheck E1 T) "cannot clear",
     E = E1
   ].
diff --git a/apps/eltac/theories/cycle.v b/apps/eltac/theories/cycle.v
new file mode 100644
index 000000000..2f1a8e4e4
--- /dev/null
+++ b/apps/eltac/theories/cycle.v
@@ -0,0 +1,30 @@
+From elpi Require Export elpi.
+
+Elpi Tactic cycle.
+Elpi Accumulate lp:{{
+
+  pred read-arg i:sealed-goal, o:list argument.
+  read-arg (nabla G) X :- pi x\ read-arg (G x) X.
+  read-arg (seal (goal _ _ _ _ A)) A.
+
+  pred cycle i:int, i:list sealed-goal, o:list sealed-goal.
+  cycle N L PL :- N > 0,
+    std.length L M,
+    std.assert! (N < M) "not enough goals",
+    std.split-at N L B A,
+    std.append A B PL.
+  cycle N L PL :- N < 0,
+    std.length L M,
+    N' is M + N,
+    cycle N' L PL.
+
+  msolve GL GS :-
+    GL = [G|_],
+    read-arg G [int N],
+    if (N = 0) (GS = GL) (cycle N GL GS).
+
+}}.
+
+Elpi Typecheck.
+
+Tactic Notation "eltac.cycle" int(n) := elpi cycle ltac_int:(n).
diff --git a/apps/eltac/theories/tactics.v b/apps/eltac/theories/tactics.v
index 8be768439..dd8f1f3b1 100644
--- a/apps/eltac/theories/tactics.v
+++ b/apps/eltac/theories/tactics.v
@@ -8,4 +8,5 @@ From elpi.apps.eltac Require Export
   generalize
   fail
   clear
+  cycle
 .
\ No newline at end of file
diff --git a/coq-builtin.elpi b/coq-builtin.elpi
index 908d435c2..990b5ef35 100644
--- a/coq-builtin.elpi
+++ b/coq-builtin.elpi
@@ -43,6 +43,7 @@ pred attributes o:list attribute.
 % Where [str "foo", int 3, trm (app[f,x])] is part of <goal>.
 % The encoding of goals is described below.
 pred solve i:goal, o:list sealed-goal.
+pred msolve i:list sealed-goal, o:list sealed-goal.
 
 % The data type of arguments (for commands or tactics)
 kind argument type.
@@ -145,7 +146,7 @@ type uvar  evarkey -> list term -> term.
 % pi x1\ decl x1 `x` <t> =>
 %  pi x2\ def x2 `y` x1 <v> =>
 %   declare-evar
-%      [decl x1 `x` <t>, def x2 `y` x1 <v>]
+%      [def x2 `y` x1 <v> , decl x1 `x` <t>]
 %      (RawEvar x1 x2) (<p> x1 x2) (Ev x1 x2)
 %
 % where, by default, declare-evar creates a syntactic constraint as
@@ -246,7 +247,7 @@ macro @holes! :- get-option "HOAS:holes" tt.
 %   nabla x2\
 %    seal
 %      (goal
-%         [decl x1 `x` <t>, def x2 `y` x1 <v>]
+%         [def x2 `y` x1 <v> , decl x1 `x` <t>]
 %         (RawEvar x1 x2) (<g> x1 x2) (Evar x1 x2)
 %         (Arguments x1 x2))
 
@@ -287,12 +288,12 @@ type goal goal-ctx -> term -> term -> term -> list argument -> goal.
 % (pi x1\ decl x1 `x` <t> =>
 %   pi x2\ def x2 `y` x1 <v> =>
 %    declare-evar
-%       [decl x1 `x` <t>, def x2 `y` x1 <v>]
+%       [def x2 `y` x1 <v> , decl x1 `x` <t>]
 %       (RawEvar x1 x2) (<g> x1 x2) (Evar x1 x2)),
 % (coq.ltac.open solve
 %  (nabla x1\ nabla x2\ seal
 %   (goal
-%     [decl x1 `x` <t>, def x2 `y` x1 <v>]
+%     [def x2 `y` x1 <v> , decl x1 `x` <t>]
 %     (RawEvar x1 x2) (<g> x1 x2) (Evar x1 x2)
 %     [int 3, str `x`, str`y`, trm (app[const `h`,x1])]))
 %   NewGoals)
@@ -1035,10 +1036,15 @@ external pred coq.strategy.get i:constant, o:conversion_strategy.
 % fail Level Msg, where Msg is the printing of the remaining arguments
 external type coq.ltac.fail int -> variadic any prop.
 
-% [coq.ltac.collect-goals T Goals ShelvedGoals] Turns the holes in T into
-% Goals. Goals are closed with nablas and equipped with GoalInfo (can be
-% left unspecified). ShelvedGoals are goals which can be solved by side
-% effect (they occur in the type of the other goals)
+% [coq.ltac.collect-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
+% in the type of the other goals).
+% 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).
+% 
 external pred coq.ltac.collect-goals i:term, o:list sealed-goal, 
                                      o:list sealed-goal.
 
diff --git a/elpi/coq-HOAS.elpi b/elpi/coq-HOAS.elpi
index ce15a7be5..05c6ba854 100644
--- a/elpi/coq-HOAS.elpi
+++ b/elpi/coq-HOAS.elpi
@@ -27,7 +27,9 @@ pred attributes o:list attribute.
 %   solve <goal> <new goals>
 % Where [str "foo", int 3, trm (app[f,x])] is part of <goal>.
 % The encoding of goals is described below.
+% msolve is for tactics that operate on multiple goals (called via all: ).
 pred solve i:goal, o:list sealed-goal.
+pred msolve i:list sealed-goal, o:list sealed-goal.
 
 % The data type of arguments (for commands or tactics)
 kind argument type.
@@ -130,7 +132,7 @@ type uvar  evarkey -> list term -> term.
 % pi x1\ decl x1 `x` <t> =>
 %  pi x2\ def x2 `y` x1 <v> =>
 %   declare-evar
-%      [decl x1 `x` <t>, def x2 `y` x1 <v>]
+%      [def x2 `y` x1 <v> , decl x1 `x` <t>]
 %      (RawEvar x1 x2) (<p> x1 x2) (Ev x1 x2)
 %
 % where, by default, declare-evar creates a syntactic constraint as
@@ -231,7 +233,7 @@ macro @holes! :- get-option "HOAS:holes" tt.
 %   nabla x2\
 %    seal
 %      (goal
-%         [decl x1 `x` <t>, def x2 `y` x1 <v>]
+%         [def x2 `y` x1 <v> , decl x1 `x` <t>]
 %         (RawEvar x1 x2) (<g> x1 x2) (Evar x1 x2)
 %         (Arguments x1 x2))
 
@@ -272,12 +274,12 @@ type goal goal-ctx -> term -> term -> term -> list argument -> goal.
 % (pi x1\ decl x1 `x` <t> =>
 %   pi x2\ def x2 `y` x1 <v> =>
 %    declare-evar
-%       [decl x1 `x` <t>, def x2 `y` x1 <v>]
+%       [def x2 `y` x1 <v> , decl x1 `x` <t>]
 %       (RawEvar x1 x2) (<g> x1 x2) (Evar x1 x2)),
 % (coq.ltac.open solve
 %  (nabla x1\ nabla x2\ seal
 %   (goal
-%     [decl x1 `x` <t>, def x2 `y` x1 <v>]
+%     [def x2 `y` x1 <v> , decl x1 `x` <t>]
 %     (RawEvar x1 x2) (<g> x1 x2) (Evar x1 x2)
 %     [int 3, str `x`, str`y`, trm (app[const `h`,x1])]))
 %   NewGoals)
@@ -307,6 +309,22 @@ type goal goal-ctx -> term -> term -> term -> list argument -> goal.
 % Ltac1 code on that term (e.g. to call vm_compute, see also the example
 % on the reflexive tactic).
 
+% ----- Multi goals tactics. ----
+% Coq provides goal selectors, such as all:, to pass to a tactic more than one
+% goal. In order to write such a tactic, Coq-Elpi provides another entry point
+% called msolve. To be precise, if there are two goals under focus, say <g1> and
+% <g2>, then all: elpi tac <t> runs the following query
+%
+%   msolve [<g1>,<g2>] NewGoals ;                         % note the disjunction
+%   coq.ltac.all (coq.ltac.open solve) [<g1>,<g2>] NewGoals
+%
+% So, if msolve has no clause, Coq-Elpi will use solve on all the goals
+% independently. If msolve has a cluse, then it can manipulate the entire list
+% of sealed goals. Note that the argument <t> is in both <g1> and <g2> but
+% it is interpreted in both contexts independently. If both goals have a proof
+% variable named "x" then passing (@eq_refl _ x) as <t> equips both goals with
+% a (raw) proof that "x = x", no matter what their type is.
+
 % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Declarations for Coq's API (environment read/write access, etc).
 % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/elpi/elpi-ltac.elpi b/elpi/elpi-ltac.elpi
index 3db34ed0a..8ff9564db 100644
--- a/elpi/elpi-ltac.elpi
+++ b/elpi/elpi-ltac.elpi
@@ -45,20 +45,20 @@ try T G GS :- T G GS.
 try _ G [G].
 
 :index(_ 1)
-pred then i:tactic, i:list sealed-goal, o:list sealed-goal.
-then T [G|Gs] O :- T G O1, then T Gs O2, std.append O1 O2 O.
-then _ [] [].
+pred all i:tactic, i:list sealed-goal, o:list sealed-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.
 thenl [] G [G].
-thenl [T|Ts] G GS :- T G NG, then (thenl Ts) NG GS.
+thenl [T|Ts] G GS :- T G NG, all (thenl Ts) NG GS.
 
 pred repeat i:tactic, i:sealed-goal, o:list sealed-goal.
-repeat T G GS :- T G GS1, then (repeat T) GS1 GS.
+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, !, then (repeat T) GS1 GS.
+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.
@@ -84,12 +84,19 @@ pred move-goal-argument i:list prop, i:list prop, i:argument, o:argument.
 move-goal-argument _ _ (int _ as A) A.
 move-goal-argument _ _ (str _ as A) A.
 move-goal-argument C D (trm T) (trm T1) :-
-  std.assert! (move-term C D T T1) "cannot move goal argument to the right context", !.
+  std.rev C Cr, std.rev D Dr,
+  std.assert! (move-term Cr Dr T T1) "cannot move goal argument to the right context", !.
 
+:index(2)
 pred move-term i:list prop, i:list prop, i:term, o:term.
 move-term [] _ T T1 :- copy T T1.
-move-term [decl X _ TX|C1] [decl Y _ TY|C2] T T1 :- same_term TX TY, !,
+move-term [decl X _ TX|C1] [decl Y _ TY|C2] T T1 :- std.do! [ copy TX TX1, same_term TX1 TY ], !,
   copy X Y => move-term C1 C2 T T1.
+move-term [def X _ TX BX|C1] [def Y _ TY BY|C2] T T1 :- std.do! [ copy TX TX1, same_term TX1 TY, copy BX BX1, same_term BX1 BY ], !,
+  copy X Y => move-term C1 C2 T T1.
+move-term [decl X _ _|C1] C2 T T1 :- not(occurs X T), !, move-term C1 C2 T T1.
+move-term [def X _ _ _|C1] C2 T T1 :- not(occurs X T), !, move-term C1 C2 T T1.
+move-term C1 [_|C2] T T1 :- move-term C1 C2 T T1.
 
 pred distribute-nabla i:(term -> list sealed-goal), o:list sealed-goal.
 distribute-nabla (_\ []) [].
diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml
index 8ebf81873..71a847daf 100644
--- a/src/coq_elpi_HOAS.ml
+++ b/src/coq_elpi_HOAS.ml
@@ -941,7 +941,7 @@ and in_elpi_evar_concl evar_concl ~raw_uvar elpi_evk coq_ctx hyps ~calldepth ~de
   let args = CList.init coq_ctx.proof_len (fun i -> E.mkConst @@ i + calldepth) in
   let hyps = List.map (fun { ctx_entry; depth = from } ->
     U.move ~from ~to_:depth ctx_entry) hyps in
-  state, U.list_to_lp_list (List.rev hyps),
+  state, U.list_to_lp_list hyps,
   (E.mkUnifVar raw_uvar ~args state),
   (E.mkUnifVar elpi_evk ~args state),
   evar_concl, gls_evar_concl
@@ -1079,14 +1079,15 @@ let preprocess_context visible context =
     ctx_hyps Int.Map.empty in
   dbl2ctx
 
+let rec dblset_of_canonical_ctx ~depth acc = function
+  | [] -> acc
+  | x :: xs ->
+      match E.look ~depth x with
+      | E.Const i -> dblset_of_canonical_ctx ~depth (Int.Set.add i acc) xs
+      | _ -> err Pp.(str"HOAS: non canonical constraint, the evar is applied to:" ++
+                      str(pp2string (P.term depth) x))
+
 let find_evar_decl var csts =
-  let rec dblset_of_canonical_ctx ~depth acc = function
-    | [] -> acc
-    | x :: xs ->
-        match E.look ~depth x with
-        | E.Const i -> dblset_of_canonical_ctx ~depth (Int.Set.add i acc) xs
-        | _ -> err Pp.(str"HOAS: non canonical constraint")
-  in
   csts |> CList.find_map (fun ({ E.goal = (depth,concl); context } as cst) ->
     match E.look ~depth concl with
     | E.App(c,x,[ty;rx]) when c == evarc ->
@@ -1493,10 +1494,12 @@ let grab_global_env_drop_univs state =
 
 
 let solvec = E.Constants.declare_global_symbol "solve"
+let msolvec = E.Constants.declare_global_symbol "msolve"
 let goalc = E.Constants.declare_global_symbol "goal"
 let nablac = E.Constants.declare_global_symbol "nabla"
 let sealc = E.Constants.declare_global_symbol "seal"
 let openc = E.Constants.declare_global_symbol "coq.ltac.open"
+let allc = E.Constants.declare_global_symbol "coq.ltac.all"
 
 let mk_goal hyps rev ty ev args =
   E.mkApp goalc hyps [rev ;ty; ev; U.list_to_lp_list args]
@@ -1504,7 +1507,7 @@ let mk_goal hyps rev ty ev args =
 let in_elpi_goal state ~args ~hyps ~raw_ev ~ty ~ev =
   mk_goal hyps raw_ev ty ev args
 
-let embed_goal ~depth ~args ~in_elpi_arg state k =
+let sealed_goal2lp ~depth ~args ~in_elpi_arg state k =
   let calldepth = depth in
   let env = get_global_env state in
   let sigma = get_sigma state in
@@ -1523,18 +1526,26 @@ let embed_goal ~depth ~args ~in_elpi_arg state k =
           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
 
-let solvegoal2query env sigma goal loc args ~in_elpi_arg ~depth:calldepth state =
-  if not (Evd.is_undefined sigma goal) then
-    err Pp.(str (Printf.sprintf "Evar %d is not a goal" (Evar.repr goal)));
+let solvegoal2query sigma goals loc args ~in_elpi_arg ~depth:calldepth state =
 
   let state = S.set command_mode state false in (* tactic mode *)
 
-  let state = S.set engine state (from_env_sigma env sigma) in
+  let state = S.set engine state (from_env_sigma (get_global_env state) sigma) in
+
+  let state, gl, gls =
+    API.Utils.map_acc (fun state goal ->
+      if not (Evd.is_undefined sigma goal) then
+        err Pp.(str (Printf.sprintf "Evar %d is not a goal" (Evar.repr goal)));
 
-  let state, g, gls = embed_goal ~depth:calldepth ~in_elpi_arg ~args state goal in
+      sealed_goal2lp ~depth:calldepth ~in_elpi_arg ~args state goal) state goals in
 
   let state, ek = F.Elpi.make ~name:"NewGoals" state in
-  let query = E.mkApp openc (E.mkConst solvec) [g;E.mkUnifVar ek ~args:[] state] in
+  let newgls = E.mkUnifVar ek ~args:[] state in
+
+  let query =
+    E.mkApp API.RawData.Constants.orc
+      (E.mkApp msolvec (U.list_to_lp_list gl) [newgls])
+      [E.mkApp allc (E.mkApp openc (E.mkConst solvec) []) [U.list_to_lp_list gl;newgls]] in
 
   let evarmap_query =
     match gls @ [query] with
@@ -1545,36 +1556,46 @@ let solvegoal2query env sigma goal loc args ~in_elpi_arg ~depth:calldepth state
   state, (loc, evarmap_query)
 ;;
 
-let customtac2query env sigma goal loc text ~depth:calldepth state =
-  if not (Evd.is_undefined sigma goal) then
-    err Pp.(str (Printf.sprintf "Evar %d is not a goal" (Evar.repr goal)));
-  let state = S.set command_mode state false in (* tactic mode *)
-  let state = S.set engine state (from_env_sigma env sigma) in
-  let state, elpi_goal_evar, elpi_raw_goal_evar, evar_decls = in_elpi_evar ~calldepth goal  state in
-  let evar_concl, goal_ctx, goal_env =
-    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 ->
-        let state, q = API.Quotation.lp ~depth state loc text in
-        state, q, []) in
-  let evarmap_query =
-    match evar_decls @ gls @ [query] with
-    | [] -> assert false
-    | [g] -> g
-    | x :: xs -> E.mkApp E.Constants.andc x xs in
-  if debug () then
-    Feedback.msg_debug Pp.(str"engine: " ++
-      str (show_coq_engine (S.get engine state)));
-  state, (loc, evarmap_query)
+let sealed_goal2lp ~depth state goal =
+  sealed_goal2lp ~depth ~args:[] ~in_elpi_arg:(fun ~depth ?calldepth _ _ _ _ _ -> assert false) state goal
+
+let customtac2query sigma goals loc text ~depth:calldepth state =
+  match goals with
+  | [] | _ :: _ :: _ ->
+     CErrors.user_err Pp.(str "elpi query can only be used on one goal")
+  | [goal] ->
+    let info = Evd.find sigma goal in
+    let env = get_global_env state in
+    let env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env in
+    if not (Evd.is_undefined sigma goal) then
+      err Pp.(str (Printf.sprintf "Evar %d is not a goal" (Evar.repr goal)));
+    let state = S.set command_mode state false in (* tactic mode *)
+    let state = S.set engine state (from_env_sigma env sigma) in
+    let state, elpi_goal_evar, elpi_raw_goal_evar, evar_decls = in_elpi_evar ~calldepth goal  state in
+    let evar_concl, goal_ctx, goal_env =
+      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 ->
+          let state, q = API.Quotation.lp ~depth state loc text in
+          state, q, []) in
+    let evarmap_query =
+      match evar_decls @ gls @ [query] with
+      | [] -> assert false
+      | [g] -> g
+      | x :: xs -> E.mkApp E.Constants.andc x xs in
+    if debug () then
+      Feedback.msg_debug Pp.(str"engine: " ++
+        str (show_coq_engine (S.get engine state)));
+    state, (loc, evarmap_query)
 ;;
 
 type 'arg tactic_main = Solve of 'arg list | Custom of string
 
-let goal2query env sigma goal loc ~main ~in_elpi_arg ~depth state =
+let goals2query sigma goals loc ~main ~in_elpi_arg ~depth state =
   match main with
-  | Solve args -> solvegoal2query env sigma goal loc args ~in_elpi_arg ~depth state
-  | Custom text -> customtac2query env sigma goal loc text ~depth state 
+  | Solve args -> solvegoal2query sigma goals loc args ~in_elpi_arg ~depth state
+  | Custom text -> customtac2query sigma goals loc text ~depth state 
 
 let eat_n_lambdas ~depth t upto state =
   let open E in
@@ -1589,12 +1610,12 @@ let eat_n_lambdas ~depth t upto state =
 
 let get_goal_ref ~depth syntactic_constraints state t =
   match E.look ~depth t with
-  | E.App(c,_,[g;_;_;i]) when c == goalc ->
+  | E.App(c,ctx,[_;_;g;i]) when c == goalc ->
      begin match E.look ~depth g with
-     | E.UnifVar(ev,_) ->
+     | E.UnifVar(ev,scope) ->
        begin try
          let uv = find_evar ev syntactic_constraints in
-         Some (UVMap.host uv state,U.lp_list_to_list ~depth i)
+         Some (ctx,UVMap.host uv state,scope,U.lp_list_to_list ~depth i)
        with Not_found -> None
        end
      | _ -> err Pp.(str"Not a variable after goal: " ++ str(pp2string (P.term depth) g))
@@ -1691,7 +1712,7 @@ let get_declared_goals all_goals constraints state assignments pp_ctx =
          let l = U.lp_list_to_list ~depth (E.kool l) in
          let declared = List.map (fun x ->
            match get_sealed_goal_ref ~depth syntactic_constraints state x with
-           | Some (g,_) -> g
+           | Some (_,g,_,_) -> g
            | None -> err Pp.(str"Not a goal " ++ str(pp2string (P.term depth) x) ++ str " in " ++ cut () ++ str(pp2string (API.Pp.constraints pp_ctx) constraints))) l in
          let declared_set =
            List.fold_right Evar.Set.add declared Evar.Set.empty in
@@ -1774,9 +1795,6 @@ let set_current_sigma ~depth state sigma =
     E.mkAppL rm_evarc [E.mkUnifVar rk ~args state; E.mkUnifVar k ~args state]) in
   state, removals @ List.concat decls @ assignments
 
-let get_goal_ref ~depth cst s t =
-  get_goal_ref ~depth (E.constraints cst) s t
-
 (* elpi -> Entries.mutual_inductive_entry **************************** *)
 
 (* documentation of the Coq API
@@ -2378,6 +2396,21 @@ let get_global_env_current_sigma ~depth hyps constraints state =
   state, coq_ctx, get_sigma state, gls
 ;;
 
+let lp2goal ~depth hyps syntactic_constraints state t =
+  match get_goal_ref ~depth (E.constraints syntactic_constraints) state t with
+  | None -> assert false
+  | Some (ctx,k,scope,args) ->
+    let state, _, changed, gl1 =
+      elpi_solution_to_coq_solution syntactic_constraints state in
+    let visible_set = dblset_of_canonical_ctx ~depth Int.Set.empty scope in
+    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 })))
+        state
+        (mk_coq_context ~options:(get_options ~depth hyps state) state) in
+    state, coq_ctx, k, args, gl1@gl2
+
 let constr2lp ~depth ?(calldepth=depth) coq_ctx _constraints state t =
   constr2lp coq_ctx ~calldepth ~depth state t
 
diff --git a/src/coq_elpi_HOAS.mli b/src/coq_elpi_HOAS.mli
index 29fc929d7..d4f20bbce 100644
--- a/src/coq_elpi_HOAS.mli
+++ b/src/coq_elpi_HOAS.mli
@@ -104,9 +104,9 @@ val in_elpi_indtdecl_field : depth:int -> State.t -> record_field_spec -> term -
 val in_elpi_indtdecl_inductive : State.t -> Vernacexpr.inductive_kind -> Names.Name.t -> term -> term list -> term
 val in_elpi_indtdecl_constructor : Names.Name.t -> term -> term
 
-val get_goal_ref : depth:int -> constraints -> State.t -> term -> (Evar.t * term list) option
-val embed_goal : depth:int -> args:'a list -> in_elpi_arg:(depth:int -> ?calldepth:int -> 'b coq_context -> 'c list -> Evd.evar_map -> State.t -> 'a -> State.t * term list * Conversion.extra_goals) ->
-  State.t -> Evar.t -> State.t * term * Conversion.extra_goals
+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
 
 (* *** Low level API to reuse parts of the embedding *********************** *)
 val unspec2opt : 'a Elpi.Builtin.unspec -> 'a option
@@ -204,8 +204,8 @@ val get_sigma : State.t -> Evd.evar_map
 type hyp = { ctx_entry : term; depth : int }
 
 type 'arg tactic_main = Solve of 'arg list | Custom of string
-val goal2query : Environ.env ->
-  Evd.evar_map -> Goal.goal -> Elpi.API.Ast.Loc.t -> main:'a tactic_main ->
+val goals2query :
+  Evd.evar_map -> Goal.goal list -> Elpi.API.Ast.Loc.t -> main:'a tactic_main ->
   in_elpi_arg:(depth:int -> ?calldepth:int -> 'b coq_context -> hyp list -> Evd.evar_map -> State.t -> 'a -> State.t * term list * Conversion.extra_goals) ->
   depth:int -> State.t -> State.t * (Elpi.API.Ast.Loc.t * term)
 val tclSOLUTION2EVD : 'a Elpi.API.Data.solution -> unit Proofview.tactic
diff --git a/src/coq_elpi_arg_HOAS.ml b/src/coq_elpi_arg_HOAS.ml
index 269d2f3fd..9b3fea423 100644
--- a/src/coq_elpi_arg_HOAS.ml
+++ b/src/coq_elpi_arg_HOAS.ml
@@ -93,29 +93,39 @@ let pr_top_ltac_arg _ _ _ = Pp.str "TODO: pr_top_ltac_arg"
 
 type ltac_ty = Int | String | Term | List of ltac_ty
 
-type ('a,'b,'c,'d,'e,'f) arg =
-  | Int of int
-  | String of string
-  | Term of 'a
-  | LTac of ltac_ty * 'f
-  | RecordDecl of 'b
-  | IndtDecl of 'c
-  | ConstantDecl of 'd
-  | Context of 'e
-
-type raw_arg = (raw_term,  raw_record_decl, raw_indt_decl, raw_constant_decl,raw_context_decl,raw_ltac_arg) arg
-type glob_arg = (glob_term, glob_record_decl, glob_indt_decl, glob_constant_decl,glob_context_decl,glob_ltac_arg) arg
-type top_arg = (top_term, top_record_decl, top_indt_decl, top_constant_decl, top_context_decl, top_ltac_arg) arg
-
- let pr_arg f g h i j k = function
+type tac
+type cmd
+
+type ('a,'b,'c,'d,'e,'f,_) arg =
+  | Int : int            -> ('a,'b,'c,'d,'e,'f,_  ) arg
+  | String : string      -> ('a,'b,'c,'d,'e,'f,_  ) arg
+  | Term : 'a            -> ('a,'b,'c,'d,'e,'f,_  ) arg
+  | LTac : ltac_ty * 'f  -> ('a,'b,'c,'d,'e,'f,tac) arg
+  | RecordDecl : 'b      -> ('a,'b,'c,'d,'e,'f,cmd) arg
+  | IndtDecl : 'c        -> ('a,'b,'c,'d,'e,'f,cmd) arg
+  | ConstantDecl : 'd    -> ('a,'b,'c,'d,'e,'f,cmd) arg
+  | Context : 'e         -> ('a,'b,'c,'d,'e,'f,cmd) arg
+
+type 'a raw_arg = (raw_term,  raw_record_decl, raw_indt_decl, raw_constant_decl,raw_context_decl,raw_ltac_arg,'a) arg
+type 'a glob_arg = (glob_term, glob_record_decl, glob_indt_decl, glob_constant_decl,glob_context_decl,glob_ltac_arg,'a) arg
+type top_arg = (top_term, top_record_decl, top_indt_decl, top_constant_decl, top_context_decl, top_ltac_arg,cmd) arg
+type top_tac_arg = (top_term, top_record_decl, top_indt_decl, top_constant_decl, top_context_decl, top_ltac_arg,tac) arg
+
+ let pr_arg f g h i j x = match x with
   | Int n -> Pp.int n
   | String s -> Pp.qstring s
   | Term s -> f s
-  | LTac(_, s) -> k s
   | RecordDecl s -> g s
   | IndtDecl s -> h s
   | ConstantDecl s -> i s
   | Context c -> j c
+
+let pr_tac_arg f k x = match x with
+  | Int n -> Pp.int n
+  | String s -> Pp.qstring s
+  | Term s -> f s
+  | LTac(_, s) -> k s
+
 let pr_glob_constr_and_expr env sigma = function
   | (_, Some c) ->
     Ppconstr.pr_constr_expr env sigma c
@@ -129,7 +139,12 @@ let pp_raw_arg env sigma =
     (pr_raw_indt_decl env sigma)
     (pr_raw_constant_decl env sigma)
     (pr_raw_context_decl env sigma)
+
+let pp_raw_tac_arg env sigma =
+  pr_tac_arg
+    (Ppconstr.pr_constr_expr env sigma)
     (pr_raw_ltac_arg env sigma)
+    
 let pp_glob_arg env sigma =
   pr_arg
     (pr_glob_constr_and_expr env sigma)
@@ -137,7 +152,12 @@ let pp_glob_arg env sigma =
     (pr_glob_indt_decl env sigma)
     (pr_glob_constant_decl env sigma)
     (pr_glob_context_decl env sigma)
+
+let pp_glob_tac_arg env sigma =
+  pr_tac_arg
+    (pr_glob_constr_and_expr env sigma)
     (pr_glob_ltac_arg env sigma)
+    
 let pp_top_arg env sigma =
   pr_arg
     (fun (_,x) -> pr_glob_constr_and_expr env sigma x)
@@ -145,8 +165,12 @@ let pp_top_arg env sigma =
     (pr_top_indt_decl env sigma)
     (pr_top_constant_decl env sigma)
     (pr_top_context_decl env sigma)
+
+let pp_top_tac_arg env sigma =
+  pr_tac_arg
+    (fun (_,x) -> pr_glob_constr_and_expr env sigma x)
     (pr_top_ltac_arg env sigma)
-    
+      
 let push_name x = function
   | Names.Name.Name id ->
       let decl = Context.Named.Declaration.LocalAssum (Context.make_annot id Sorts.Relevant, Constr.mkProp) in
@@ -282,11 +306,16 @@ let subst_constant_decl s { name; params; typ; body } =
   let body = Option.map (subst_global_constr s) body in
   { name; params; typ; body }
 
+let glob_tac_arg glob_sign = function
+  | Int _ as x -> glob_sign, x
+  | String _ as x -> glob_sign, x
+  | Term t -> glob_sign, Term (intern_tactic_constr glob_sign t)
+  | LTac(ty,t) -> glob_sign, LTac (ty,fst @@ intern_tactic_constr glob_sign t)
+  
 let glob_arg glob_sign = function
   | Int _ as x -> x
   | String _ as x -> x
   | Term t -> Term (intern_tactic_constr glob_sign t)
-  | LTac(ty,t) -> LTac (ty,fst @@ intern_tactic_constr glob_sign t)
   | RecordDecl t -> RecordDecl (intern_record_decl glob_sign t)
   | IndtDecl t -> IndtDecl (intern_indt_decl glob_sign t)
   | ConstantDecl t -> ConstantDecl (intern_constant_decl glob_sign t)
@@ -297,8 +326,6 @@ let subst_arg mod_subst = function
   | String _ as x -> x
   | Term t ->
       Term (Ltac_plugin.Tacsubst.subst_glob_constr_and_expr mod_subst t)
-  | LTac(ty,t) ->
-      LTac(ty,(Detyping.subst_glob_constr (Global.env()) mod_subst t))
   | RecordDecl t ->
       RecordDecl (subst_record_decl mod_subst t)
   | IndtDecl t ->
@@ -308,22 +335,54 @@ let subst_arg mod_subst = function
   | Context t ->
       Context (subst_context_decl mod_subst t)
 
+let subst_tac_arg mod_subst = function
+  | Int _ as x -> x
+  | String _ as x -> x
+  | Term t ->
+      Term (Ltac_plugin.Tacsubst.subst_glob_constr_and_expr mod_subst t)
+  | LTac(ty,t) ->
+      LTac(ty,(Detyping.subst_glob_constr (Global.env()) mod_subst t))    
 
 let interp_arg ist evd = function
   | Int _ as x -> evd.Evd.sigma, x
   | String _ as x -> evd.Evd.sigma, x
   | Term t -> evd.Evd.sigma, Term(ist,t)
-  | LTac(ty,v) ->
-      let id =
-        match DAst.get v with
-        | Glob_term.GVar id -> id
-        | _ -> assert false in
-      evd.Evd.sigma, LTac(ty,(ist,id))
   | RecordDecl t -> evd.Evd.sigma, (RecordDecl(ist,t))
   | IndtDecl t -> evd.Evd.sigma, (IndtDecl(ist,t))
   | ConstantDecl t -> evd.Evd.sigma, (ConstantDecl(ist,t))
   | Context c -> evd.Evd.sigma, (Context(ist,c))
 
+let interp_tac_arg return ist = function
+| Int _ as x -> return x
+| String _ as x -> return x
+| Term t -> return @@ Term(ist,t)
+| LTac(ty,v) ->
+    let id =
+      match DAst.get v with
+      | Glob_term.GVar id -> id
+      | _ -> assert false in
+      return @@ LTac(ty,(ist,id))
+
+let add_genarg tag pr_raw pr_glob pr_top glob subst interp =
+  let wit = Genarg.make0 tag in
+  let tag = Geninterp.Val.create tag in
+  let () = Genintern.register_intern0 wit glob in
+  let () = Genintern.register_subst0 wit subst in
+  let () = Geninterp.register_interp0 wit (interp (fun x -> Ftactic.return @@ Geninterp.Val.Dyn (tag, x))) in
+  let () = Geninterp.register_val0 wit (Some (Geninterp.Val.Base tag)) in
+  Ltac_plugin.Pptactic.declare_extra_genarg_pprule wit pr_raw pr_glob pr_top;
+  wit
+;;
+
+let wit_elpi_ftactic_arg = add_genarg "elpi_ftactic_arg"
+  (fun env sigma _ _ _ -> pp_raw_tac_arg env sigma)
+  (fun env sigma _ _ _ -> pp_glob_tac_arg env sigma)
+  (fun env sigma _ _ _ -> pp_top_tac_arg env sigma)
+  glob_tac_arg
+  subst_tac_arg
+  interp_tac_arg
+
+
 
 let grecord2lp ~depth state { name; arity; params; constructorname; fields } =
   let open Coq_elpi_glob_quotation in
@@ -433,6 +492,29 @@ let to_list v =
   | None -> raise (Taccoerce.CannotCoerceTo "a list")
   | Some l -> l
 
+type 'a constr2lp = depth:int ->
+    ?calldepth:int ->
+    ([> `Options] as 'a) Coq_elpi_HOAS.coq_context ->
+    Elpi__API.Data.constraints ->
+    Elpi__API.Data.state ->
+    Evd.econstr ->
+    Elpi__API.Data.state * Elpi__API.Data.term * Elpi__API.Data.term list
+
+let in_elpi_common_arg_aux :
+  type a.
+  depth:int -> ?calldepth:int -> 'c coq_context -> hyp list -> Evd.evar_map -> API.State.t -> constr2lp: 'c constr2lp -> (_,_,_,_,_,_,a) arg -> API.State.t * E.term list * API.Conversion.extra_goals = fun
+ ~depth ?calldepth coq_ctx hyps sigma state ~constr2lp x ->
+   match x with
+   | String x -> state, [E.mkApp strc (CD.of_string x) []], []
+   | Int x -> state, [E.mkApp intc (CD.of_int x) []], []
+   | Term (ist,glob_or_expr) ->
+       let closure = Ltac_plugin.Tacinterp.interp_glob_closure ist coq_ctx.env sigma glob_or_expr in
+       let g = Coq_elpi_utils.detype_closed_glob coq_ctx.env sigma closure in
+       let state = Coq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in
+       let state, t = Coq_elpi_glob_quotation.gterm2lp ~depth state g in
+       state, [E.mkApp trmc t []], []
+   | _ -> assert false
+ 
 let rec in_elpi_ltac_arg ~depth ?calldepth coq_ctx hyps sigma state ~constr2lp ty ist v =
   let open Ltac_plugin in
   let in_elpi_arg state = in_elpi_arg_aux ~depth ?calldepth coq_ctx hyps sigma state ~constr2lp in
@@ -472,15 +554,7 @@ let rec in_elpi_ltac_arg ~depth ?calldepth coq_ctx hyps sigma state ~constr2lp t
       with Taccoerce.CannotCoerceTo _ ->
         raise (Taccoerce.CannotCoerceTo "a term")
 
-and in_elpi_arg_aux ~depth ?calldepth coq_ctx hyps sigma state ~constr2lp = function
-  | String x -> state, [E.mkApp strc (CD.of_string x) []], []
-  | Int x -> state, [E.mkApp intc (CD.of_int x) []], []
-  | Term (ist,glob_or_expr) ->
-      let closure = Ltac_plugin.Tacinterp.interp_glob_closure ist coq_ctx.env sigma glob_or_expr in
-      let g = Coq_elpi_utils.detype_closed_glob coq_ctx.env sigma closure in
-      let state = Coq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in
-      let state, t = Coq_elpi_glob_quotation.gterm2lp ~depth state g in
-      state, [E.mkApp trmc t []], []
+and in_elpi_tac_arg_aux ~depth ?calldepth coq_ctx hyps sigma state ~constr2lp = function
   | LTac(ty,(ist,id)) ->
       let v = try Id.Map.find id ist.Geninterp.lfun with Not_found -> assert false in
       begin try
@@ -488,6 +562,9 @@ and in_elpi_arg_aux ~depth ?calldepth coq_ctx hyps sigma state ~constr2lp = func
       with Ltac_plugin.Taccoerce.CannotCoerceTo s ->
         let env = Some (coq_ctx.env,sigma) in
         Ltac_plugin.Taccoerce.error_ltac_variable id env v s end
+  | x -> in_elpi_common_arg_aux ~depth ?calldepth coq_ctx hyps sigma state ~constr2lp x
+
+and in_elpi_arg_aux ~depth ?calldepth coq_ctx hyps sigma state ~constr2lp = function
   | RecordDecl (_ist,glob_rdecl) ->
       let state = Coq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in
       let state, t = grecord2lp ~depth state glob_rdecl in
@@ -505,11 +582,12 @@ and in_elpi_arg_aux ~depth ?calldepth coq_ctx hyps sigma state ~constr2lp = func
       let state = Coq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in
       let state, t = do_context glob_ctx ~depth state in
       state, [E.mkApp ctxc t []], []
+  | x -> in_elpi_common_arg_aux ~depth ?calldepth coq_ctx hyps sigma state ~constr2lp x
+    
+let in_elpi_tac_arg ~depth ?calldepth coq_ctx hyps sigma state t =
+  in_elpi_tac_arg_aux ~depth ?calldepth coq_ctx hyps sigma state ~constr2lp:Coq_elpi_HOAS.constr2lp t
 
-let in_elpi_arg ~depth ?calldepth coq_ctx hyps sigma state t =
-  in_elpi_arg_aux ~depth ?calldepth coq_ctx hyps sigma state ~constr2lp:Coq_elpi_HOAS.constr2lp t
-
-let in_elpi_global_arg ~depth ?calldepth coq_ctx state arg =
+let in_elpi_arg ~depth ?calldepth coq_ctx state arg =
   let state, args, gls =
     in_elpi_arg_aux ~depth ?calldepth coq_ctx [] (Evd.from_env coq_ctx.env) ~constr2lp:Coq_elpi_HOAS.constr2lp_closed_ground state arg in
   assert(gls = []); (* only ltac args can generate evars and hence extra goals *)
@@ -517,20 +595,22 @@ let in_elpi_global_arg ~depth ?calldepth coq_ctx state arg =
   | [arg] -> state, arg
   | _ -> assert false (* ltac arguments are not global *)
 
-type coq_arg = Cint of int | Cstr of string | Ctrm of E.term
+type coq_arg = Cint of int | Cstr of string | Ctrm of EConstr.t
 
-let in_coq_arg ~depth state t =
+let in_coq_arg ~depth proof_context constraints state t =
   match E.look ~depth t with
   | E.App(c,i,[]) when c == intc ->
       begin match E.look ~depth i with
-      | E.CData c when CD.is_int c -> Cint (CD.to_int c)
+      | E.CData c when CD.is_int c -> state, Cint (CD.to_int c), []
       | _ -> raise API.Conversion.(TypeErr (TyName"argument",depth,t))
       end
   | E.App(c,s,[]) when c == strc ->
       begin match E.look ~depth s with
-      | E.CData c when CD.is_string c -> Cstr (CD.to_string c)
+      | E.CData c when CD.is_string c -> state, Cstr (CD.to_string c), []
       | _ -> raise API.Conversion.(TypeErr (TyName"argument",depth,t))
       end
-  | E.App(c,t,[]) when c == trmc -> Ctrm t
+  | E.App(c,t,[]) when c == trmc ->
+      let state, t, gls = lp2constr ~depth proof_context constraints state t in
+      state, Ctrm t, gls
   | _ -> raise API.Conversion.(TypeErr (TyName"argument",depth,t))
 
diff --git a/src/coq_elpi_arg_HOAS.mli b/src/coq_elpi_arg_HOAS.mli
index 1902b97de..bfe3aa660 100644
--- a/src/coq_elpi_arg_HOAS.mli
+++ b/src/coq_elpi_arg_HOAS.mli
@@ -68,46 +68,58 @@ type top_ltac_arg = Geninterp.interp_sign * Names.Id.t
 
 type ltac_ty = Int | String | Term | List of ltac_ty
 
-type ('a,'b,'c,'d,'e,'f) arg =
-  | Int of int
-  | String of string
-  | Term of 'a
-  | LTac of ltac_ty * 'f
-  | RecordDecl of 'b
-  | IndtDecl of 'c
-  | ConstantDecl of 'd
-  | Context of 'e
-
-type raw_arg = (raw_term,  raw_record_decl, raw_indt_decl, raw_constant_decl,raw_context_decl,raw_term) arg
-type glob_arg = (glob_term, glob_record_decl, glob_indt_decl, glob_constant_decl,glob_context_decl,Glob_term.glob_constr) arg
-type top_arg = (top_term, top_record_decl, top_indt_decl, top_constant_decl, top_context_decl, top_ltac_arg) arg
-
-val pp_raw_arg : Environ.env -> Evd.evar_map -> raw_arg -> Pp.t
-val pp_glob_arg : Environ.env -> Evd.evar_map -> glob_arg -> Pp.t
+type tac
+type cmd
+
+type ('a,'b,'c,'d,'e,'f,_) arg =
+  | Int : int            -> ('a,'b,'c,'d,'e,'f,_  ) arg
+  | String : string      -> ('a,'b,'c,'d,'e,'f,_  ) arg
+  | Term : 'a            -> ('a,'b,'c,'d,'e,'f,_  ) arg
+  | LTac : ltac_ty * 'f  -> ('a,'b,'c,'d,'e,'f,tac) arg
+  | RecordDecl : 'b      -> ('a,'b,'c,'d,'e,'f,cmd) arg
+  | IndtDecl : 'c        -> ('a,'b,'c,'d,'e,'f,cmd) arg
+  | ConstantDecl : 'd    -> ('a,'b,'c,'d,'e,'f,cmd) arg
+  | Context : 'e         -> ('a,'b,'c,'d,'e,'f,cmd) arg
+
+type 'a raw_arg = (raw_term,  raw_record_decl, raw_indt_decl, raw_constant_decl,raw_context_decl,raw_term,'a) arg
+type 'a glob_arg = (glob_term, glob_record_decl, glob_indt_decl, glob_constant_decl,glob_context_decl,Glob_term.glob_constr,'a) arg
+type top_arg = (top_term, top_record_decl, top_indt_decl, top_constant_decl, top_context_decl, top_ltac_arg,cmd) arg
+type top_tac_arg = (top_term, top_record_decl, top_indt_decl, top_constant_decl, top_context_decl, top_ltac_arg,tac) arg
+
+val pp_raw_arg : Environ.env -> Evd.evar_map -> cmd raw_arg -> Pp.t
+val pp_glob_arg : Environ.env -> Evd.evar_map -> cmd glob_arg -> Pp.t
 val pp_top_arg : Environ.env -> Evd.evar_map -> top_arg -> Pp.t
 
-val glob_arg : Genintern.glob_sign -> raw_arg -> glob_arg
-val interp_arg : Geninterp.interp_sign -> 'g Evd.sigma -> glob_arg -> Evd.evar_map * top_arg
-val subst_arg : Mod_subst.substitution -> glob_arg -> glob_arg
+val glob_arg : Genintern.glob_sign -> cmd raw_arg -> cmd glob_arg
+val interp_arg : Geninterp.interp_sign -> 'g Evd.sigma -> cmd glob_arg -> Evd.evar_map * top_arg
+val subst_arg : Mod_subst.substitution -> cmd glob_arg -> cmd glob_arg
+
+val wit_elpi_ftactic_arg : (tac raw_arg, tac glob_arg, top_tac_arg) Genarg.genarg_type
 
 (* for tactics *)
-val in_elpi_arg :
+val in_elpi_tac_arg :
   depth:int -> ?calldepth:int -> 
   Coq_elpi_HOAS.full Coq_elpi_HOAS.coq_context ->
   Coq_elpi_HOAS.hyp list ->
   Evd.evar_map ->
   Elpi.API.State.t ->
-  top_arg ->
+  top_tac_arg ->
   Elpi.API.State.t * term list * Elpi.API.Conversion.extra_goals
 
 (* for commands *)
-val in_elpi_global_arg :
+val in_elpi_arg :
   depth:int -> ?calldepth:int -> 
   Coq_elpi_HOAS.empty Coq_elpi_HOAS.coq_context ->
   Elpi.API.State.t ->
   top_arg ->
   Elpi.API.State.t * term
 
-type coq_arg = Cint of int | Cstr of string | Ctrm of term
+type coq_arg = Cint of int | Cstr of string | Ctrm of EConstr.t
 
-val in_coq_arg : depth:int -> Elpi.API.State.t -> term -> coq_arg
+val in_coq_arg :
+  depth:int ->
+  Coq_elpi_HOAS.full Coq_elpi_HOAS.coq_context ->
+  Elpi.API.Data.constraints ->
+  Elpi.API.State.t ->
+  term ->
+    Elpi.API.State.t * coq_arg * Elpi.API.Conversion.extra_goals
diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index b4b7efee6..951acdc15 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -286,8 +286,24 @@ let term_skeleton =  {
 }
 
 let prop = { B.any with Conv.ty = Conv.TyName "prop" }
-let raw_closed_goal = { B.any with Conv.ty = Conv.TyName "sealed-goal" }
-let raw_goal = { B.any with Conv.ty = Conv.TyName "goal" }
+let sealed_goal = {
+  Conv.ty = Conv.TyName "sealed-goal";
+  pp_doc = (fun fmt () -> ());
+  pp = (fun fmt _ -> Format.fprintf fmt "TODO");
+  embed = sealed_goal2lp;
+  readback = (fun ~depth _ _ -> assert false);
+}
+
+let goal : ( (Coq_elpi_HOAS.full Coq_elpi_HOAS.coq_context * Evar.t * Coq_elpi_arg_HOAS.coq_arg list) , 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 = Coq_elpi_HOAS.lp2goal ~depth hyps csts state g in
+    let state, args, gls2 = API.Utils.map_acc (Coq_elpi_arg_HOAS.in_coq_arg ~depth ctx csts) state raw_args in
+    state, (ctx,k,args), gls1 @ gls2);
+}
 
 let id = { B.string with
   API.Conversion.ty = Conv.TyName "id";
@@ -2286,9 +2302,16 @@ coq.reduction.vm.whd_all T TY R :-
 
   MLCode(Pred("coq.ltac.collect-goals",
     CIn(failsafe_term, "T",
-    Out(list raw_closed_goal, "Goals",
-    Out(list raw_closed_goal, "ShelvedGoals",
-    Full(proof_context, "Turns the holes in T into Goals. Goals are closed with nablas and equipped with GoalInfo (can be left unspecified). ShelvedGoals are goals which can be solved by side effect (they occur in the type of the other goals)")))),
+    Out(list sealed_goal, "Goals",
+    Out(list sealed_goal, "ShelvedGoals",
+    Full(proof_context, {|
+Turns the holes in T into Goals.
+Goals are closed with nablas.
+ShelvedGoals are goals which can be solved by side effect (they occur
+in the type of the other goals).
+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 sigma = get_sigma state in
       let evars_of_term evd c =
@@ -2318,38 +2341,26 @@ coq.reduction.vm.whd_all T TY R :-
           (fun g ->
              CList.exists (fun (tgt, lazy evs) -> not (Evar.equal g tgt) && Evar.Set.mem g evs) free_evars)
           subgoals in
-      let state, subgoals, gls = API.Utils.map_acc (embed_goal ~depth ~args:[] ~in_elpi_arg:Coq_elpi_arg_HOAS.in_elpi_arg) state subgoals in
-      let state, shelved, gls2 =
+      let shelved =
         match shelved with
-        | Keep ->
-           let state, shelved, gls2 =
-             API.Utils.map_acc (embed_goal ~depth ~args:[] ~in_elpi_arg:Coq_elpi_arg_HOAS.in_elpi_arg) state shelved_subgoals in
-           state, Some shelved, gls2
-        | Discard -> state, None, [] in
-      state, !: subgoals +? shelved, gls @ gls2
+        | Keep -> Some shelved_subgoals
+        | Discard -> None in
+      state, !: subgoals +? shelved, []
     )),
     DocAbove);
 
   MLCode(Pred("coq.ltac.call-ltac1",
     In(B.string, "Tac",
-    In(raw_goal, "G",
-    Out(list raw_closed_goal,"GL",
-    Full(proof_context, "Calls Ltac1 tactic named Tac on goal G (passing the arguments of G, see coq.ltac.call for a handy wrapper)")))),
-    (fun tac_name goal _ ~depth proof_context constraints state ->
+    CIn(goal, "G",
+    Out(list sealed_goal,"GL",
+    Full(raw_ctx, "Calls Ltac1 tactic named Tac on goal G (passing the arguments of G, see coq.ltac.call for a handy wrapper)")))),
+    (fun tac_name (proof_context,goal,tac_args) _ ~depth _ _ state ->
       let open Ltac_plugin in
       let sigma = get_sigma state in
-       let goal, goal_args =
-         match get_goal_ref ~depth constraints state goal with
-         | None -> raise Conv.(TypeErr (TyName"goal",depth,goal))
-         | Some (k, args) -> k, args in
-       let state, tac_args, gls1 =
-         API.Utils.map_acc (fun state x ->
-           match Coq_elpi_arg_HOAS.in_coq_arg ~depth state x with
-           | Coq_elpi_arg_HOAS.Ctrm t ->
-              let state, t, gl = term.CConv.readback ~depth proof_context constraints state t in
-              state, Tacinterp.Value.of_constr t, gl
-           | Coq_elpi_arg_HOAS.Cstr s -> state, Geninterp.(Val.inject (val_tag (Genarg.topwit Stdarg.wit_string))) s, []
-           | Coq_elpi_arg_HOAS.Cint i -> state, Tacinterp.Value.of_int i, []) state goal_args in
+       let tac_args = tac_args |> List.map (function
+         | Coq_elpi_arg_HOAS.Ctrm t -> Tacinterp.Value.of_constr t
+         | Coq_elpi_arg_HOAS.Cstr s -> Geninterp.(Val.inject (val_tag (Genarg.topwit Stdarg.wit_string))) s
+         | Coq_elpi_arg_HOAS.Cint i -> Tacinterp.Value.of_int i) in
        let tactic =
          let tac_name =
            let q = Libnames.qualid_of_string tac_name in
@@ -2372,14 +2383,12 @@ coq.reduction.vm.whd_all T TY R :-
            try
              apply ~name:(Id.of_string "elpi") ~poly:false proof_context.env focused_tac pv
            with e when CErrors.noncritical e ->
-             (* Feedback.msg_debug (CErrors.print e); *)
+             Feedback.msg_debug (CErrors.print e);
              raise Pred.No_clause
          in
            proofview pv in
        let state, assignments = set_current_sigma ~depth state sigma in
-       let state, subgoals, gls2 =
-         API.Utils.map_acc (embed_goal ~depth ~args:[] ~in_elpi_arg:Coq_elpi_arg_HOAS.in_elpi_arg) state subgoals in
-       state, !: subgoals, gls1 @ assignments @ gls2
+       state, !: subgoals, assignments
       )),
   DocAbove);
 
diff --git a/src/coq_elpi_builtins_HOAS.ml b/src/coq_elpi_builtins_HOAS.ml
index 1419c7bfe..3ef4b5cb1 100644
--- a/src/coq_elpi_builtins_HOAS.ml
+++ b/src/coq_elpi_builtins_HOAS.ml
@@ -30,6 +30,7 @@ pred attributes o:list attribute.
 % Where [str "foo", int 3, trm (app[f,x])] is part of <goal>.
 % The encoding of goals is described below.
 pred solve i:goal, o:list sealed-goal.
+pred msolve i:list sealed-goal, o:list sealed-goal.
 
 % The data type of arguments (for commands or tactics)
 kind argument type.
@@ -132,7 +133,7 @@ type uvar  evarkey -> list term -> term.
 % pi x1\ decl x1 `x` <t> =>
 %  pi x2\ def x2 `y` x1 <v> =>
 %   declare-evar
-%      [decl x1 `x` <t>, def x2 `y` x1 <v>]
+%      [def x2 `y` x1 <v> , decl x1 `x` <t>]
 %      (RawEvar x1 x2) (<p> x1 x2) (Ev x1 x2)
 %
 % where, by default, declare-evar creates a syntactic constraint as
@@ -233,7 +234,7 @@ macro @holes! :- get-option "HOAS:holes" tt.
 %   nabla x2\
 %    seal
 %      (goal
-%         [decl x1 `x` <t>, def x2 `y` x1 <v>]
+%         [def x2 `y` x1 <v> , decl x1 `x` <t>]
 %         (RawEvar x1 x2) (<g> x1 x2) (Evar x1 x2)
 %         (Arguments x1 x2))
 
@@ -274,12 +275,12 @@ type goal goal-ctx -> term -> term -> term -> list argument -> goal.
 % (pi x1\ decl x1 `x` <t> =>
 %   pi x2\ def x2 `y` x1 <v> =>
 %    declare-evar
-%       [decl x1 `x` <t>, def x2 `y` x1 <v>]
+%       [def x2 `y` x1 <v> , decl x1 `x` <t>]
 %       (RawEvar x1 x2) (<g> x1 x2) (Evar x1 x2)),
 % (coq.ltac.open solve
 %  (nabla x1\ nabla x2\ seal
 %   (goal
-%     [decl x1 `x` <t>, def x2 `y` x1 <v>]
+%     [def x2 `y` x1 <v> , decl x1 `x` <t>]
 %     (RawEvar x1 x2) (<g> x1 x2) (Evar x1 x2)
 %     [int 3, str `x`, str`y`, trm (app[const `h`,x1])]))
 %   NewGoals)
diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml
index a88399416..80412d624 100644
--- a/src/coq_elpi_vernacular.ml
+++ b/src/coq_elpi_vernacular.ml
@@ -618,7 +618,7 @@ let run_program loc name ~atts args =
     |> List.map snd in
   let query ~depth state =
     let state, args = Coq_elpi_utils.list_map_acc
-      (Coq_elpi_arg_HOAS.in_elpi_global_arg ~depth Coq_elpi_HOAS.(mk_coq_context ~options:default_options state))
+      (Coq_elpi_arg_HOAS.in_elpi_arg ~depth Coq_elpi_HOAS.(mk_coq_context ~options:default_options state))
       state args in
     let state, q = atts2impl loc ~depth state atts (ET.mkApp mainc (EU.list_to_lp_list args) []) in
     state, (loc, q) in
@@ -670,13 +670,16 @@ let print name args =
   run_and_print ~tactic_mode:false ~print:false ~static_check:false (compile ["Elpi";"Print"] [printer ()] []) (`Fun q)
 ;;
 
-open Proofview
 open Tacticals.New
 
-let run_tactic_common loc ?(static_check=false) program ~main ?(atts=[]) gl env sigma =
-  let k = Goal.goal gl in
+let run_tactic_common loc ?(static_check=false) program ~main ?(atts=[]) () =
+  let open Proofview in
+  let open Notations in
+  Unsafe.tclGETGOALS >>= fun gls ->
+  let gls = CList.map Proofview.drop_state gls in
+  Proofview.tclEVARMAP >>= fun sigma ->
   let query ~depth state = 
-    let state, (loc, q) = Coq_elpi_HOAS.goal2query env sigma k loc ~main ~in_elpi_arg:Coq_elpi_arg_HOAS.in_elpi_arg ~depth state in
+    let state, (loc, q) = Coq_elpi_HOAS.goals2query sigma gls loc ~main ~in_elpi_arg:Coq_elpi_arg_HOAS.in_elpi_tac_arg ~depth state in
     let state, qatts = atts2impl loc ~depth state atts q in
     state, (loc, qatts)
     in
@@ -689,18 +692,10 @@ let run_tactic_common loc ?(static_check=false) program ~main ?(atts=[]) gl env
 
 let run_tactic loc program ~atts _ist args =
   let loc = Coq_elpi_utils.of_coq_loc loc in
-  Goal.enter begin fun gl ->
-  tclBIND tclEVARMAP begin fun sigma -> 
-  tclBIND tclENV begin fun env ->
-  run_tactic_common loc program ~main:(Coq_elpi_HOAS.Solve args) ~atts gl env sigma
-end end end
+  run_tactic_common loc program ~main:(Coq_elpi_HOAS.Solve args) ~atts ()
 
 let run_in_tactic ?(program = current_program ()) (loc,query) _ist =
-  Goal.enter begin fun gl ->
-  tclBIND tclEVARMAP begin fun sigma ->
-  tclBIND tclENV begin fun env -> 
-  run_tactic_common loc ~static_check:true program ~main:(Coq_elpi_HOAS.Custom query) gl env sigma
-end end end
+  run_tactic_common loc ~static_check:true program ~main:(Coq_elpi_HOAS.Custom query) ()
 
 let accumulate_files ?(program=current_program()) s =
   let elpi = ensure_initialized () in
@@ -742,9 +737,9 @@ let loc_merge l1 l2 =
 
 open Coq_elpi_arg_HOAS
 
-let in_exported_program : (qualified_name * (Loc.t,Loc.t,Loc.t) Genarg.ArgT.tag * (raw_arg,glob_arg,top_arg) Genarg.ArgT.tag * (raw_arg,glob_arg,top_arg) Genarg.ArgT.tag * (Attributes.vernac_flags,Attributes.vernac_flags,Attributes.vernac_flags) Genarg.ArgT.tag) -> Libobject.obj =
+let in_exported_program : (qualified_name * (Loc.t,Loc.t,Loc.t) Genarg.ArgT.tag * (cmd raw_arg, cmd glob_arg,top_arg) Genarg.ArgT.tag * (Attributes.vernac_flags,Attributes.vernac_flags,Attributes.vernac_flags) Genarg.ArgT.tag) -> Libobject.obj =
   Libobject.declare_object @@ Libobject.global_object_nodischarge "ELPI-EXPORTED"
-    ~cache:(fun (_,(p,tag_loc,tag_arg,tag_tacticarg,tag_attributes)) ->
+    ~cache:(fun (_,(p,tag_loc,tag_arg,tag_attributes)) ->
       let p_str = String.concat "." p in
       match get_nature p with
       | Command ->
@@ -765,8 +760,8 @@ let in_exported_program : (qualified_name * (Loc.t,Loc.t,Loc.t) Genarg.ArgT.tag
           CErrors.user_err Pp.(str "elpi: Only commands can be exported"))
     ~subst:(Some (fun _ -> CErrors.user_err Pp.(str"elpi: No functors yet")))
 
-let export_command p tag_loc tag_arg tag_tacticarg tag_attributes =
-  Lib.add_anonymous_leaf (in_exported_program (p,tag_loc,tag_arg,tag_tacticarg,tag_attributes))
+let export_command p tag_loc tag_arg tag_attributes =
+  Lib.add_anonymous_leaf (in_exported_program (p,tag_loc,tag_arg,tag_attributes))
 
 let skip ~atts:(skip,only) f x =
   let m rex = Str.string_match rex Coq_config.version 0 in
diff --git a/src/coq_elpi_vernacular.mli b/src/coq_elpi_vernacular.mli
index ce5705b13..2d510fec6 100644
--- a/src/coq_elpi_vernacular.mli
+++ b/src/coq_elpi_vernacular.mli
@@ -36,16 +36,15 @@ val print : qualified_name -> string list -> unit
 
 open Coq_elpi_arg_HOAS
 
-val run_program : Loc.t -> qualified_name -> atts:Attributes.vernac_flags -> raw_arg list -> unit
+val run_program : Loc.t -> qualified_name -> atts:Attributes.vernac_flags -> cmd raw_arg list -> unit
 val run_in_program : ?program:qualified_name -> Elpi.API.Ast.Loc.t * string -> unit
-val run_tactic : Loc.t -> qualified_name -> atts:Attributes.vernac_flags -> Geninterp.interp_sign -> top_arg list -> unit Proofview.tactic
+val run_tactic : Loc.t -> qualified_name -> atts:Attributes.vernac_flags -> Geninterp.interp_sign -> top_tac_arg list -> unit Proofview.tactic
 val run_in_tactic : ?program:qualified_name -> Elpi.API.Ast.Loc.t * string -> Geninterp.interp_sign -> unit Proofview.tactic
 
 val export_command :
   qualified_name ->
   (Loc.t,Loc.t,Loc.t) Genarg.ArgT.tag ->
-  (raw_arg,glob_arg,top_arg) Genarg.ArgT.tag ->
-  (raw_arg,glob_arg,top_arg) Genarg.ArgT.tag ->
+  (cmd raw_arg,cmd glob_arg,top_arg) Genarg.ArgT.tag ->
   (Attributes.vernac_flags,Attributes.vernac_flags,Attributes.vernac_flags) Genarg.ArgT.tag ->
   unit
 
diff --git a/src/coq_elpi_vernacular_syntax.mlg b/src/coq_elpi_vernacular_syntax.mlg
index fa56d2fa1..33867a52a 100644
--- a/src/coq_elpi_vernacular_syntax.mlg
+++ b/src/coq_elpi_vernacular_syntax.mlg
@@ -207,6 +207,8 @@ let any_kwd = Pcoq.Entry.of_parser "any_symbols_or_kwd" any_kwd
 let pr_attributes _ _ _ atts =
   Pp.(prlist_with_sep (fun () -> str ",") Attributes.pr_vernac_flag atts)
 
+let wit_elpi_ftactic_arg = EA.wit_elpi_ftactic_arg
+
 }
 
 GRAMMAR EXTEND Gram
@@ -283,12 +285,7 @@ GLOB_PRINTED BY { fun _ _ _ -> EA.pp_glob_arg env sigma }
 END
 
 ARGUMENT EXTEND elpi_tactic_arg
-PRINTED BY { fun _ _ _ -> EA.pp_top_arg env sigma }
-INTERPRETED BY { EA.interp_arg }
-GLOBALIZED BY { EA.glob_arg }
-SUBSTITUTED BY { EA.subst_arg }
-RAW_PRINTED BY { fun _ _ _ -> EA.pp_raw_arg env sigma }
-GLOB_PRINTED BY { fun _ _ _ -> EA.pp_glob_arg env sigma }
+TYPED AS elpi_ftactic_arg
 | [ qualified_name(s) ] -> { EA.String (String.concat "." (snd s)) }
 | [ integer(n) ] -> { EA.Int n }
 | [ string(s) ] -> { EA.String s }
@@ -391,7 +388,6 @@ VERNAC COMMAND EXTEND ElpiRun CLASSIFIED BY { fun _ -> Vernacextend.(VtSideff ([
     EV.export_command (snd p)
       (Genarg.get_arg_tag wit_elpi_loc)
       (Genarg.get_arg_tag wit_elpi_arg)
-      (Genarg.get_arg_tag wit_elpi_tactic_arg)
       (Genarg.get_arg_tag wit_attributes)
   }
 | #[ atts = any_attribute ]
diff --git a/tests/test_tactic.v b/tests/test_tactic.v
index c57a343e9..5b6f3ca7d 100644
--- a/tests/test_tactic.v
+++ b/tests/test_tactic.v
@@ -111,7 +111,7 @@ solve (goal Ctx _Ev (prod _ T x\ app[G x,B x,_]) _ _) _ :-
     coq.typecheck (B x) (Ty x) ok,
     coq.typecheck (G x) (GTy x) ok,
     coq.say [B,Ty,G,GTy],
-    {std.rev Ctx} = [decl X _ _|_],
+    Ctx = [decl X _ _|_],
     H = {{lp:X = 2}},
     coq.typecheck H HT ok, % X is restricted wrt x
     coq.say [H,HT]
@@ -278,3 +278,23 @@ Fail (#[ bar ] testatt).
 Fail (#[ foo2 ] testatt).
 testatt #[ foo ].
 Abort.
+
+(* ***************** *)
+
+Elpi Tactic test_m.
+Elpi Accumulate lp:{{
+  type type-arg open-tactic.
+  type-arg (goal _ _ _ _ [trm T] as G) GL :-
+    refine T G GL.
+
+  msolve GL New :-
+    coq.ltac.all (coq.ltac.open type-arg) GL New.
+}}.
+Elpi Typecheck.
+
+Goal (forall x : nat, x = x) /\ (forall x : bool, x = x).
+split; intro x.
+all: elpi test_m (@eq_refl _ x).
+Qed.
+
+
diff --git a/theories/wip/memoization.v b/theories/wip/memoization.v
index 574aa9f95..61752439a 100644
--- a/theories/wip/memoization.v
+++ b/theories/wip/memoization.v
@@ -43,7 +43,7 @@ Elpi Accumulate lp:{{
     memo-db DB, memo-lookup DB Ty P, coq.say "hit" Ty, !.
 
   repeat-memo T (goal _ _ Ty Proof _ as G) GS :-
-    T (seal G) New, coq.ltac.then (coq.ltac.open (repeat-memo T)) New GS,
+    T (seal G) New, coq.ltac.all (coq.ltac.open (repeat-memo T)) New GS,
     if (GS = []) (memo-db DB, stash_in_safe DB (item Ty Proof)) true.
 
 }}.