aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacsubst.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tacsubst.ml')
-rw-r--r--tactics/tacsubst.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 55941c1ca..4059877b7 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -299,6 +299,7 @@ let () =
Genintern.register_subst0 wit_var (fun _ v -> v);
Genintern.register_subst0 wit_intro_pattern (fun _ v -> v);
Genintern.register_subst0 wit_tactic subst_tactic;
+ Genintern.register_subst0 wit_ltac subst_tactic;
Genintern.register_subst0 wit_constr subst_glob_constr;
Genintern.register_subst0 wit_sort (fun _ v -> v);
Genintern.register_subst0 wit_clause_dft_concl (fun _ v -> v);