diff options
Diffstat (limited to 'plugins/ltac/tacinterp.ml')
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 12a31ad164..8ddf17ca14 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2029,7 +2029,8 @@ let () = register_interp0 wit_pre_ident (lift interp_pre_ident); register_interp0 wit_ident (lift interp_ident); register_interp0 wit_var (lift interp_hyp); - register_interp0 wit_intro_pattern (lifts interp_intro_pattern); + register_interp0 wit_intropattern (lifts interp_intro_pattern) [@warning "-3"]; + register_interp0 wit_simple_intropattern (lifts interp_intro_pattern); register_interp0 wit_clause_dft_concl (lift interp_clause); register_interp0 wit_constr (lifts interp_constr); register_interp0 wit_tacvalue (fun ist v -> Ftactic.return v); |