diff options
| author | ppedrot | 2012-12-14 09:26:08 +0000 |
|---|---|---|
| committer | ppedrot | 2012-12-14 09:26:08 +0000 |
| commit | 9330bf650ca602884c5c4c69c2fb3e94ee32838b (patch) | |
| tree | 5947d599c9c408680236995b11a47ab93703b701 /intf/constrexpr.mli | |
| parent | 02077f5b5e132e135be778c201e74a5eb87b97ae (diff) | |
Implemented a full-fledged equality on [constr_expr]. By the way,
some cleaning of the interface and moving of code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16066 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'intf/constrexpr.mli')
| -rw-r--r-- | intf/constrexpr.mli | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 3225284796..01380b8d5a 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -65,16 +65,15 @@ type constr_expr = | CRef of reference | 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 + | CProdN of Loc.t * binder_expr list * constr_expr + | CLambdaN of Loc.t * binder_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.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.t * cases_pattern_expr list located list * constr_expr) list + case_expr list * branch_expr list | CLetTuple of Loc.t * name located list * (name located option * constr_expr option) * constr_expr * constr_expr | CIf of Loc.t * constr_expr * (name located option * constr_expr option) @@ -89,6 +88,15 @@ type constr_expr = | CPrim of Loc.t * prim_token | CDelimiters of Loc.t * string * constr_expr +and case_expr = + constr_expr * (name located option * cases_pattern_expr option) + +and branch_expr = + Loc.t * cases_pattern_expr list located list * constr_expr + +and binder_expr = + name located list * binder_kind * constr_expr + and fix_expr = identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr |