diff options
Diffstat (limited to 'plugins/ltac/tacintern.ml')
| -rw-r--r-- | plugins/ltac/tacintern.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 0fa4dc8baf..3ed5b1aab2 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -795,7 +795,8 @@ let () = let ist = { ist with ltacvars = !lf } in (ist, ans) in - Genintern.register_intern0 wit_intro_pattern intern_intro_pattern + Genintern.register_intern0 wit_intropattern intern_intro_pattern [@warning "-3"]; + Genintern.register_intern0 wit_simple_intropattern intern_intro_pattern let () = let intern_clause ist cl = |