From 83e22b5abc05902d1468d1cf033251dae46b69bc Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 17 Mar 2020 10:37:30 +0100 Subject: 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 --- interp/notation_term.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'interp/notation_term.ml') diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 29db23cc54..c541a19bfd 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -67,7 +67,8 @@ type extended_subscopes = Constrexpr.notation_entry_level * subscopes type constr_as_binder_kind = | AsIdent - | AsIdentOrPattern + | AsName + | AsNameOrPattern | AsStrictPattern type notation_binder_source = @@ -76,6 +77,8 @@ type notation_binder_source = | NtnParsedAsPattern of bool (* This accepts only ident *) | NtnParsedAsIdent + (* This accepts only name *) + | NtnParsedAsName (* This accepts ident, or pattern, or both *) | NtnBinderParsedAsConstr of constr_as_binder_kind (* This accepts ident, _, and quoted pattern *) -- cgit v1.2.3