diff options
Diffstat (limited to 'plugins/ltac/pltac.ml')
| -rw-r--r-- | plugins/ltac/pltac.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml index 28ab801ee2..e3042dc3cb 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -52,7 +52,9 @@ let () = let open Stdarg in let open Tacarg in register_grammar wit_int_or_var (int_or_var); - register_grammar wit_intro_pattern (simple_intropattern); + register_grammar wit_intro_pattern (simple_intropattern); (* To remove at end of deprecation phase *) +(* register_grammar wit_intropattern (intropattern); *) (* To be added at end of deprecation phase *) + register_grammar wit_simple_intropattern (simple_intropattern); register_grammar wit_quant_hyp (quantified_hypothesis); register_grammar wit_uconstr (uconstr); register_grammar wit_open_constr (open_constr); |