Improve tactic interpreter registration API a bit

Using it feels nicer this way, with GADT details hidden inside comtactic

5 files changed, 13 insertions, 10 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/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