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 --- parsing/extend.ml | 2 ++ parsing/extend.mli | 2 ++ 2 files changed, 4 insertions(+) (limited to 'parsing') diff --git a/parsing/extend.ml b/parsing/extend.ml index 94c3768116..7d2ed9aed0 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -32,6 +32,7 @@ let production_level_eq lev1 lev2 = type 'a constr_entry_key_gen = | ETIdent + | ETName of bool (* Temporary: true = user told "name", false = user wrote "ident" *) | ETGlobal | ETBigint | ETBinder of bool (* open list of binders if true, closed list of binders otherwise *) @@ -55,6 +56,7 @@ type binder_entry_kind = ETBinderOpen | ETBinderClosed of string Tok.p list type binder_target = ForBinder | ForTerm type constr_prod_entry_key = + | ETProdIdent (* Parsed as an ident *) | ETProdName (* Parsed as a name (ident or _) *) | ETProdReference (* Parsed as a global reference *) | ETProdBigint (* Parsed as an (unbounded) integer *) diff --git a/parsing/extend.mli b/parsing/extend.mli index b698415fd6..3cea45c3f5 100644 --- a/parsing/extend.mli +++ b/parsing/extend.mli @@ -27,6 +27,7 @@ val production_level_eq : production_level -> production_level -> bool type 'a constr_entry_key_gen = | ETIdent + | ETName of bool (* Temporary: true = user told "name", false = user wrote "ident" *) | ETGlobal | ETBigint | ETBinder of bool (* open list of binders if true, closed list of binders otherwise *) @@ -50,6 +51,7 @@ type binder_entry_kind = ETBinderOpen | ETBinderClosed of string Tok.p list type binder_target = ForBinder | ForTerm type constr_prod_entry_key = + | ETProdIdent (* Parsed as an ident *) | ETProdName (* Parsed as a name (ident or _) *) | ETProdReference (* Parsed as a global reference *) | ETProdBigint (* Parsed as an (unbounded) integer *) -- cgit v1.2.3