diff options
Diffstat (limited to 'ltac/tacsubst.ml')
| -rw-r--r-- | ltac/tacsubst.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml index 55de58361..b09bdda65 100644 --- a/ltac/tacsubst.ml +++ b/ltac/tacsubst.ml @@ -291,6 +291,7 @@ and subst_genarg subst (GenArg (Glbwit wit, x)) = let () = Genintern.register_subst0 wit_int_or_var (fun _ v -> v); Genintern.register_subst0 wit_ref subst_global_reference; + Genintern.register_subst0 wit_pre_ident (fun _ v -> v); Genintern.register_subst0 wit_ident (fun _ v -> v); Genintern.register_subst0 wit_var (fun _ v -> v); Genintern.register_subst0 wit_intro_pattern (fun _ v -> v); |