diff options
Diffstat (limited to 'intf/constrexpr.mli')
| -rw-r--r-- | intf/constrexpr.mli | 71 |
1 files changed, 36 insertions, 35 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 605be512c..d8387b9df 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Loc open Pp open Names open Libnames @@ -36,27 +37,27 @@ type proj_flag = int option (** [Some n] = proj of the n-th visible argument *) type prim_token = Numeral of Bigint.bigint | String of string type raw_cases_pattern_expr = - | RCPatAlias of loc * raw_cases_pattern_expr * identifier - | RCPatCstr of loc * Globnames.global_reference + | RCPatAlias of Loc.t * raw_cases_pattern_expr * identifier + | RCPatCstr of Loc.t * Globnames.global_reference * raw_cases_pattern_expr list * raw_cases_pattern_expr list (** [CPatCstr (_, Inl c, l1, l2)] represents (@c l1) l2 *) - | RCPatAtom of loc * identifier option - | RCPatOr of loc * raw_cases_pattern_expr list + | RCPatAtom of Loc.t * identifier option + | RCPatOr of Loc.t * raw_cases_pattern_expr list type cases_pattern_expr = - | CPatAlias of loc * cases_pattern_expr * identifier - | CPatCstr of loc * reference + | CPatAlias of Loc.t * cases_pattern_expr * identifier + | CPatCstr of Loc.t * reference * cases_pattern_expr list * cases_pattern_expr list (** [CPatCstr (_, Inl c, l1, l2)] represents (@c l1) l2 *) - | CPatAtom of loc * reference option - | CPatOr of loc * cases_pattern_expr list - | CPatNotation of loc * notation * cases_pattern_notation_substitution + | CPatAtom of Loc.t * reference option + | CPatOr of Loc.t * cases_pattern_expr list + | CPatNotation of Loc.t * notation * cases_pattern_notation_substitution * cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents (notation n applied with substitution l1) applied to arguments l2 *) - | CPatPrim of loc * prim_token - | CPatRecord of loc * (reference * cases_pattern_expr) list - | CPatDelimiters of loc * string * cases_pattern_expr + | CPatPrim of Loc.t * prim_token + | CPatRecord of Loc.t * (reference * cases_pattern_expr) list + | CPatDelimiters of Loc.t * string * cases_pattern_expr and cases_pattern_notation_substitution = cases_pattern_expr list * (** for constr subterms *) @@ -64,31 +65,31 @@ and cases_pattern_notation_substitution = type constr_expr = | CRef of reference - | CFix of loc * identifier located * fix_expr list - | CCoFix of loc * identifier located * cofix_expr list - | CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr - | CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr - | CLetIn of loc * name located * constr_expr * constr_expr - | CAppExpl of loc * (proj_flag * reference) * constr_expr list - | CApp of loc * (proj_flag * constr_expr) * + | CFix of Loc.t * identifier located * fix_expr list + | CCoFix of Loc.t * identifier located * cofix_expr list + | CProdN of Loc.t * (name located list * binder_kind * constr_expr) list * constr_expr + | CLambdaN of Loc.t * (name located list * binder_kind * constr_expr) list * constr_expr + | CLetIn of Loc.t * name located * constr_expr * constr_expr + | CAppExpl of Loc.t * (proj_flag * reference) * constr_expr list + | CApp of Loc.t * (proj_flag * constr_expr) * (constr_expr * explicitation located option) list - | CRecord of loc * constr_expr option * (reference * constr_expr) list - | CCases of loc * case_style * constr_expr option * + | CRecord of Loc.t * constr_expr option * (reference * constr_expr) list + | CCases of Loc.t * case_style * constr_expr option * (constr_expr * (name located option * cases_pattern_expr option)) list * - (loc * cases_pattern_expr list located list * constr_expr) list - | CLetTuple of loc * name located list * (name located option * constr_expr option) * + (Loc.t * cases_pattern_expr list located list * constr_expr) list + | CLetTuple of Loc.t * name located list * (name located option * constr_expr option) * constr_expr * constr_expr - | CIf of loc * constr_expr * (name located option * constr_expr option) + | CIf of Loc.t * constr_expr * (name located option * constr_expr option) * constr_expr * constr_expr - | CHole of loc * Evar_kinds.t option - | CPatVar of loc * (bool * patvar) - | CEvar of loc * existential_key * constr_expr list option - | CSort of loc * glob_sort - | CCast of loc * constr_expr * constr_expr cast_type - | CNotation of loc * notation * constr_notation_substitution - | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr - | CPrim of loc * prim_token - | CDelimiters of loc * string * constr_expr + | CHole of Loc.t * Evar_kinds.t option + | CPatVar of Loc.t * (bool * patvar) + | CEvar of Loc.t * existential_key * constr_expr list option + | CSort of Loc.t * glob_sort + | CCast of Loc.t * constr_expr * constr_expr cast_type + | CNotation of Loc.t * notation * constr_notation_substitution + | CGeneralization of Loc.t * binding_kind * abstraction_kind option * constr_expr + | CPrim of Loc.t * prim_token + | CDelimiters of Loc.t * string * constr_expr and fix_expr = identifier located * (identifier located option * recursion_order_expr) * @@ -126,5 +127,5 @@ type with_declaration_ast = type module_ast = | CMident of qualid located - | CMapply of loc * module_ast * module_ast - | CMwith of loc * module_ast * with_declaration_ast + | CMapply of Loc.t * module_ast * module_ast + | CMwith of Loc.t * module_ast * with_declaration_ast |