Generalizing the notion of constr substitution to generic arguments.

This removes a dependency on wit_tactic in Constrintern.

1 files changed, 15 insertions, 0 deletions

diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index f51cc3518f..b1de30893d 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -794,3 +794,18 @@ let () =
   Genintern.register_intern0 wit_constr_with_bindings (lift intern_constr_with_bindings);
   Genintern.register_intern0 wit_destruction_arg (lift intern_destruction_arg);
   ()
+
+(** Substitution for notations containing tactic-in-terms *)
+
+let notation_subst bindings tac =
+  let fold id c accu =
+    let loc = Glob_ops.loc_of_glob_constr (fst c) in
+    let c = ConstrMayEval (ConstrTerm c) in
+    ((loc, id), c) :: accu
+  in
+  let bindings = Id.Map.fold fold bindings [] in
+  (** This is theoretically not correct due to potential variable capture, but
+      Ltac has no true variables so one cannot simply substitute *)
+  TacLetIn (false, bindings, tac)
+
+let () = Genintern.register_ntn_subst0 wit_tactic notation_subst