Merge PR #13167: Ltac2: use ComTactic infrastructure

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

3 files changed, 4 insertions, 4 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. *)