From 9330bf650ca602884c5c4c69c2fb3e94ee32838b Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Fri, 14 Dec 2012 09:26:08 +0000
Subject: 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
---
 intf/constrexpr.mli | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

(limited to 'intf')

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
-- 
cgit v1.2.3