diff options
| author | Hugo Herbelin | 2020-03-17 10:37:30 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-22 13:28:40 +0100 |
| commit | 83e22b5abc05902d1468d1cf033251dae46b69bc (patch) | |
| tree | 561e9f5bcdbf6d76bbf7b7cbe002aa6773cdca25 /interp/notation.ml | |
| parent | 9c841105fe2b51305abcba7bd8a574705dbd1adf (diff) | |
Renaming "ident" into "name" in grammar entries, to prevent confusions.
We use a deprecation phase where:
- "ident" means "name" (as it used to mean), except in custom coercion
entries where it already meant "ident".
- "ident" will be made again available (outside situation of
coercions) to mean "ident" at the end of deprecation phase.
Also renaming "as ident" into "as name".
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index b5951a9c59..c35ba44aa5 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -62,10 +62,11 @@ let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 let notation_binder_source_eq s1 s2 = match s1, s2 with | NtnParsedAsIdent, NtnParsedAsIdent -> true +| NtnParsedAsName, NtnParsedAsName -> true | NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2 | NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2 | NtnParsedAsBinder, NtnParsedAsBinder -> true -| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _ | NtnParsedAsBinder), _ -> false +| (NtnParsedAsIdent | NtnParsedAsName | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _ | NtnParsedAsBinder), _ -> false let ntpe_eq t1 t2 = match t1, t2 with | NtnTypeConstr, NtnTypeConstr -> true |