diff options
| author | Hugo Herbelin | 2020-08-30 08:20:29 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-10 23:19:32 +0200 |
| commit | 8d27b12365a1d8b3f1670a055537dd3724583baf (patch) | |
| tree | 40421ea2f267c51a2c0a3b96328784e40909dc9a /interp/notation_ops.ml | |
| parent | 2a50e04a58c97cf8a973b6e15ba5de326f3366e5 (diff) | |
Notations: reworking the treatment of only-parsing and only-printing notations.
The (old) original model for notations was to associated both a
parsing and a printing rule to a notation.
Progressively, it become more and more common to have only parsing
notations or even multiple expressions printed with the same notation.
The new model is to attach to a given scope, string and entry at most
one either only-parsing or mixed-parsing-printing rules + an
arbitrarily many unrelated only-printing rules.
Additionally, we anticipate the ability to selectively
activate/deactivate each of those.
This allows to fix in particular #9682 but also to have
more-to-the-point warnings in case a notation overrides or partially
overrides another one.
Rules for importing are not changed (see forthcoming #12984 though).
We also improve the output of "Print Scopes" so that it adds when a
notation is only-parsing, only-printing, or deactivated, or a
combination of those.
Fixes #4738
Fixes #9682
Fixes part 2 of #12908
Fixes #13112
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 22531b0016..354809252e 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -27,7 +27,9 @@ open Notation_term (* helper for NVar, NVar case in eq_notation_constr *) let get_var_ndx id vs = try Some (List.index Id.equal id vs) with Not_found -> None -let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with +let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = +(vars1 == vars2 && t1 == t2) || +match t1, t2 with | NRef gr1, NRef gr2 -> GlobRef.equal gr1 gr2 | NVar id1, NVar id2 -> ( match (get_var_ndx id1 vars1,get_var_ndx id2 vars2) with |