diff options
| author | coqbot-app[bot] | 2020-11-23 15:06:48 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-23 15:06:48 +0000 |
| commit | 5fce39e0078935662fd6fb9b8e2ee6b0da60b3ab (patch) | |
| tree | efc105da1f224ef87400e4bab4779670b8057827 /parsing/extend.ml | |
| parent | 94d579844817edcbb2454dd9dc79071b2cd1d12a (diff) | |
| parent | 87c46c50506089ba16bdd7afd7e795ee21033319 (diff) | |
Merge PR #11841: Distinguishing entry "ident" from entry "name" in term notations.
Reviewed-by: jfehrle
Reviewed-by: gares
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
Diffstat (limited to 'parsing/extend.ml')
| -rw-r--r-- | parsing/extend.ml | 2 |
1 files changed, 2 insertions, 0 deletions
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 *) |