Merge PR #13167: Ltac2: use ComTactic infrastructure

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

2 files changed, 9 insertions, 6 deletions

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