Merge PR #13167: Ltac2: use ComTactic infrastructure

Reviewed-by: ejgallego
Reviewed-by: gares
Reviewed-by: ppedrot

8 files changed, 25 insertions, 28 deletions

diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 6cf5d30a95..2d74323689 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -402,7 +402,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve STATE proof
     { classify_as_proofstep } -> {
     let g = Option.default (Goal_select.get_default_goal_selector ()) g in
     let global = match g with Goal_select.SelectAll | Goal_select.SelectList _ -> true | _ -> false in
-    let t = ComTactic.I (Tacinterp.hide_interp, { Tacinterp.global; ast = t; }) in
+    let t = Tacinterp.hide_interp { Tacinterp.global; ast = t; } in
     ComTactic.solve g ~info t ~with_end_tac
   }
 END
@@ -415,7 +415,7 @@ VERNAC { tactic_mode } EXTEND VernacSolveParallel STATE proof
       VtProofStep{ proof_block_detection = pbr }
     } -> {
       let t, abstract = rm_abstract t in
-      let t = ComTactic.I (Tacinterp.hide_interp, { Tacinterp.global = true; ast = t; }) in
+      let t = Tacinterp.hide_interp { Tacinterp.global = true; ast = t; } in
       ComTactic.solve_parallel ~info t ~abstract ~with_end_tac
     }
 END
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 12bfb4d09e..22b9abda20 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2019,7 +2019,7 @@ let hide_interp {global;ast} =
       hide_interp (Proofview.Goal.env gl)
     end
 
-let hide_interp = ComTactic.register_tactic_interpreter "ltac1" hide_interp
+let ComTactic.Interpreter hide_interp = ComTactic.register_tactic_interpreter "ltac1" hide_interp
 
 (***************************************************************************)
 (** Register standard arguments *)
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index 01d7306c9d..dba9c938ec 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -131,7 +131,7 @@ type tactic_expr = {
   ast:  Tacexpr.raw_tactic_expr;
 }
 
-val hide_interp : tactic_expr ComTactic.tactic_interpreter
+val hide_interp : tactic_expr -> ComTactic.interpretable
 
 (** Internals that can be useful for syntax extensions. *)
 
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} *)
 
diff --git a/vernac/comTactic.ml b/vernac/comTactic.ml
index 8a9a412362..2252d46e58 100644
--- a/vernac/comTactic.ml
+++ b/vernac/comTactic.ml
@@ -16,13 +16,13 @@ module DMap = Dyn.Map(struct type 'a t = 'a -> unit Proofview.tactic end)
 
 let interp_map = ref DMap.empty
 
-type 'a tactic_interpreter = 'a Dyn.tag
-type interpretable = I : 'a tactic_interpreter * 'a -> interpretable
+type interpretable = I : 'a Dyn.tag * 'a -> interpretable
+type 'a tactic_interpreter = Interpreter of ('a -> interpretable)
 
 let register_tactic_interpreter na f =
   let t = Dyn.create na in
   interp_map := DMap.add t f !interp_map;
-  t
+  Interpreter (fun x -> I (t,x))
 
 let interp_tac (I (tag,t)) =
   let f = DMap.find tag !interp_map in
diff --git a/vernac/comTactic.mli b/vernac/comTactic.mli
index f1a75e1b6a..72e71d013a 100644
--- a/vernac/comTactic.mli
+++ b/vernac/comTactic.mli
@@ -9,10 +9,13 @@
 (************************************************************************)
 
 (** Tactic interpreters have to register their interpretation function *)
-type 'a tactic_interpreter
-type interpretable = I : 'a tactic_interpreter * 'a -> interpretable
+type interpretable
 
-(** ['a] should be marshallable if ever used with [par:] *)
+type 'a tactic_interpreter = private Interpreter of ('a -> interpretable)
+
+(** ['a] should be marshallable if ever used with [par:]. Must be
+    called no more than once per process with a particular string: make
+    sure to use partial application. *)
 val register_tactic_interpreter :
   string -> ('a -> unit Proofview.tactic) -> 'a tactic_interpreter