diff options
| author | Hugo Herbelin | 2019-09-23 19:53:11 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-09-23 21:04:56 +0200 |
| commit | eed41b6b570755aa4b40e2ce308c57db88ec9a18 (patch) | |
| tree | 5436724966a7a87a912c2d533cf50c7a0a23a8c5 /plugins | |
| parent | dc690e7067aa91a05472b5d573cb463223ef4dec (diff) | |
Fixes #10778 (fresh was not updated after renaming of intropattern entry in #10239).
The bug was introduced in #10239 which seems to have actually remained
half-done: "wit_intropattern" and "wit_simple_intropattern" did not
share the same representation of values (val_tag) but the code was
assuming (especially the code for "fresh") that this was shared.
We fix it by sharing the internal representation (`dyn` field in
Tacarg.make0) as suggested by @ppedrot in the discussion of #10239
(this allows also to simplify Taccoerce.is_intro_pattern).
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 |