Ltac2: use ComTactic infrastructure

3 files changed, 12 insertions, 18 deletions

diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 5ae8f4ae6e..cecc6c66d2 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -920,10 +920,10 @@ open Vernacextend
 }
 
 VERNAC { tac2mode } EXTEND VernacLtac2
-| ![proof] [ ltac2_expr(t) ltac_use_default(default) ] =>
+| ![proof] [ ltac2_expr(t) ltac_use_default(with_end_tac) ] =>
     { classify_as_proofstep } -> {
 (*     let g = Option.default (Proof_global.get_default_goal_selector ()) g in *)
-  fun ~pstate -> Tac2entries.call ~pstate ~default t }
+  fun ~pstate -> Tac2entries.call ~pstate ~with_end_tac t }
 END
 
 GRAMMAR EXTEND Gram
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 30340cd632..03789fff6c 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -911,25 +911,19 @@ let print_ltac qid =
 
 (** Calling tactics *)
 
-let solve ~pstate default tac =
-  let pstate, status = Declare.Proof.map_fold_endline pstate ~f:(fun etac p ->
-    let with_end_tac = if default then Some etac else None in
-    let g = Goal_select.get_default_goal_selector () in
-    let (p, status) = Proof.solve g None tac ?with_end_tac p in
-    (* in case a strict subtree was completed,
-       go back to the top of the prooftree *)
-    let p = Proof.maximal_unfocus Vernacentries.command_focus p in
-    p, status)
-  in
-  if not status then Feedback.feedback Feedback.AddedAxiom;
-  pstate
-
-let call ~pstate ~default e =
+let ltac2_interp e =
   let loc = e.loc in
   let (e, t) = intern ~strict:false [] e in
   let () = check_unit ?loc t in
   let tac = Tac2interp.interp Tac2interp.empty_environment e in
-  solve ~pstate default (Proofview.tclIGNORE tac)
+  Proofview.tclIGNORE tac
+
+let ComTactic.Interpreter ltac2_interp = ComTactic.register_tactic_interpreter "ltac2" ltac2_interp
+
+let call ~pstate ~with_end_tac tac =
+  ComTactic.solve ~pstate ~with_end_tac
+    (Goal_select.get_default_goal_selector())
+    ~info:None (ltac2_interp tac)
 
 (** Primitive algebraic types than can't be defined Coq-side *)
 
diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli
index fc56a54e3a..2f053df2d0 100644
--- a/user-contrib/Ltac2/tac2entries.mli
+++ b/user-contrib/Ltac2/tac2entries.mli
@@ -53,7 +53,7 @@ val print_ltac : Libnames.qualid -> unit
 (** {5 Eval loop} *)
 
 (** Evaluate a tactic expression in the current environment *)
-val call : pstate:Declare.Proof.t -> default:bool -> raw_tacexpr -> Declare.Proof.t
+val call : pstate:Declare.Proof.t -> with_end_tac:bool -> raw_tacexpr -> Declare.Proof.t
 
 (** {5 Toplevel exceptions} *)