diff options
| author | Hugo Herbelin | 2019-09-29 00:06:19 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-19 21:09:07 +0100 |
| commit | 039b2423cf7b85f2f5960dde6a1586f0f07cf9d0 (patch) | |
| tree | 1fe4fd03177b52af4dd0e3a4f04b92fedd93ae71 /interp/constrexpr.ml | |
| parent | 9dc88f3c146aeaf8151fcef6ac45ca50675d052b (diff) | |
Addressing #6082 and #7766 (overriding format of notation).
We do two changes:
- We distinguish between a notion of format generically attached to
notations and a new notion of format attached to interpreted
notations. "Reserved Notation" attaches a format
generically. "Notation" attaches the format specifically to the given
interpretation, and additionally, attaches it generically if it is the
first time the notation is defined.
- We warn before overriding an explicitly reserved generic format, or
a specific format.
Diffstat (limited to 'interp/constrexpr.ml')
| -rw-r--r-- | interp/constrexpr.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index b96ef7c4e5..1d51109b7f 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -19,11 +19,17 @@ type universe_decl_expr = (lident list, Glob_term.glob_constraint list) UState.g type ident_decl = lident * universe_decl_expr option type name_decl = lname * universe_decl_expr option +type notation_with_optional_scope = LastLonelyNotation | NotationInScope of string type notation_entry = InConstrEntry | InCustomEntry of string type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * int type notation_key = string + +(* A notation associated to a given parsing rule *) type notation = notation_entry_level * notation_key +(* A notation associated to a given interpretation *) +type specific_notation = notation_with_optional_scope * notation + type 'a or_by_notation_r = | AN of 'a | ByNotation of (string * string option) @@ -78,7 +84,7 @@ type cases_pattern_expr_r = (** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *) | CPatAtom of qualid option | CPatOr of cases_pattern_expr list - | CPatNotation of notation * cases_pattern_notation_substitution + | CPatNotation of notation_with_optional_scope option * notation * cases_pattern_notation_substitution * cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents (notation n applied with substitution l1) applied to arguments l2 *) @@ -119,7 +125,7 @@ and constr_expr_r = | CEvar of Glob_term.existential_name * (Id.t * constr_expr) list | CSort of Glob_term.glob_sort | CCast of constr_expr * constr_expr Glob_term.cast_type - | CNotation of notation * constr_notation_substitution + | CNotation of notation_with_optional_scope option * notation * constr_notation_substitution | CGeneralization of Glob_term.binding_kind * abstraction_kind option * constr_expr | CPrim of prim_token | CDelimiters of string * constr_expr |