diff options
| author | Pierre-Marie Pédrot | 2019-09-25 14:30:59 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-09-25 14:30:59 +0200 |
| commit | 4e022849b7119e3a51b46fa73132b3e3cc7927ab (patch) | |
| tree | 67430007168765a36c4df6ff348eff1dfbb0ae92 /plugins | |
| parent | 092fa59dd892ea99ee17cae03da9dffe5ab3007f (diff) | |
| parent | eed41b6b570755aa4b40e2ce308c57db88ec9a18 (diff) | |
Merge PR #10781: Fixes #10778 (fresh was not updated after renaming of intropattern entry in #10239)
Reviewed-by: ppedrot
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 |