diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.ml | 5 | ||||
| -rw-r--r-- | intf/extend.ml | 10 | ||||
| -rw-r--r-- | intf/intf.mllib | 2 | ||||
| -rw-r--r-- | intf/notation_term.ml | 6 |
4 files changed, 13 insertions, 10 deletions
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml index 2575b71ea5..c598287943 100644 --- a/intf/constrexpr.ml +++ b/intf/constrexpr.ml @@ -46,7 +46,7 @@ type prim_token = type instance_expr = Misctypes.glob_level list type cases_pattern_expr_r = - | CPatAlias of cases_pattern_expr * Id.t + | CPatAlias of cases_pattern_expr * Name.t Loc.located | CPatCstr of reference * cases_pattern_expr list option * cases_pattern_expr list (** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *) @@ -128,7 +128,8 @@ and local_binder_expr = and constr_notation_substitution = constr_expr list * (** for constr subterms *) constr_expr list list * (** for recursive notations *) - local_binder_expr list list (** for binders subexpressions *) + cases_pattern_expr list * (** for binders *) + local_binder_expr list list (** for binder lists (recursive notations) *) type constr_pattern_expr = constr_expr diff --git a/intf/extend.ml b/intf/extend.ml index 79bbbd376e..5258ef56b8 100644 --- a/intf/extend.ml +++ b/intf/extend.ml @@ -37,13 +37,13 @@ type ('lev,'pos) constr_entry_key_gen = | ETBigint | ETBinder of bool (* open list of binders if true, closed list of binders otherwise *) | ETConstr of ('lev * 'pos) - | ETPattern + | ETPattern of int | ETOther of string * string -(** Entries level (left-hand-side of grammar rules) *) +(** Entries level (left-hand side of grammar rules) *) type constr_entry_key = - (int,unit) constr_entry_key_gen + (production_level,production_position) constr_entry_key_gen (** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *) @@ -54,12 +54,14 @@ type simple_constr_prod_entry_key = type binder_entry_kind = ETBinderOpen | ETBinderClosed of Tok.t list +type binder_target = ForBinder | ForTerm + type constr_prod_entry_key = | ETProdName (* Parsed as a name (ident or _) *) | ETProdReference (* Parsed as a global reference *) | ETProdBigint (* Parsed as an (unbounded) integer *) | ETProdConstr of (production_level * production_position) (* Parsed as constr or pattern *) - | ETProdPattern (* Parsed as pattern (as subpart of a constr) *) + | ETProdPattern of int (* Parsed as pattern as a binder (as subpart of a constr) *) | ETProdOther of string * string (* Intended for embedding custom entries in constr or pattern *) | ETProdConstrList of (production_level * production_position) * Tok.t list (* Parsed as non-empty list of constr *) | ETProdBinderList of binder_entry_kind (* Parsed as non-empty list of local binders *) diff --git a/intf/intf.mllib b/intf/intf.mllib index 38a2a71cc0..2b8960d3f2 100644 --- a/intf/intf.mllib +++ b/intf/intf.mllib @@ -2,9 +2,9 @@ Constrexpr Evar_kinds Genredexpr Locus +Extend Notation_term Decl_kinds -Extend Glob_term Misctypes Pattern diff --git a/intf/notation_term.ml b/intf/notation_term.ml index 52fd0f368f..83cc454f43 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -61,13 +61,13 @@ type subscopes = tmp_scope_name option * scope_name list (** Type of the meta-variables of an notation_constr: in a recursive pattern x..y, x carries the sequence of objects bound to the list x..y *) type notation_var_instance_type = - | NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList + | NtnTypeConstr | NtnTypeBinder of bool | NtnTypeConstrList | NtnTypeBinderList (** Type of variables when interpreting a constr_expr as a notation_constr: in a recursive pattern x..y, both x and y carry the individual type of each element of the list x..y *) type notation_var_internalization_type = - | NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent + | NtnInternTypeAny | NtnInternTypeOnlyBinder (** This characterizes to what a notation is interpreted to *) type interpretation = @@ -95,7 +95,7 @@ type precedence = int type parenRelation = L | E | Any | Prec of precedence type tolerability = precedence * parenRelation -type level = precedence * tolerability list * notation_var_internalization_type list +type level = precedence * tolerability list * Extend.constr_entry_key list (** Grammar rules for a notation *) |