diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/tacarg.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/taccoerce.ml | 7 |
2 files changed, 3 insertions, 6 deletions
diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml index 9e8e86d4fc..252c15478d 100644 --- a/plugins/ltac/tacarg.ml +++ b/plugins/ltac/tacarg.ml @@ -20,7 +20,7 @@ let make0 ?dyn name = wit let wit_intropattern = make0 "intropattern" (* To keep after deprecation phase but it will get a different parsing semantics (Tactic Notation and TACTIC EXTEND) in pltac.ml *) -let wit_simple_intropattern = make0 "simple_intropattern" +let wit_simple_intropattern = make0 ~dyn:(val_tag (topwit wit_intropattern)) "simple_intropattern" let wit_quant_hyp = make0 "quant_hyp" let wit_constr_with_bindings = make0 "constr_with_bindings" let wit_open_constr_with_bindings = make0 "open_constr_with_bindings" diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index e64129d204..da89a027e2 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -145,11 +145,8 @@ let coerce_to_constr_context v = else raise (CannotCoerceTo "a term context") let is_intro_pattern v = - if has_type v (topwit wit_intropattern [@warning "-3"]) then - Some (out_gen (topwit wit_intropattern [@warning "-3"]) v).CAst.v - else - if has_type v (topwit wit_simple_intropattern) then - Some (out_gen (topwit wit_simple_intropattern) v).CAst.v + if has_type v (topwit wit_intro_pattern) then + Some (out_gen (topwit wit_intro_pattern) v).CAst.v else None |