From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 intf/constrexpr.mli | 37 ++++++++++++++++++++++++-------------
 1 file changed, 24 insertions(+), 13 deletions(-)

(limited to 'intf/constrexpr.mli')

diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index dcdbd47f..0cbb2957 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -32,21 +32,25 @@ type abstraction_kind = AbsLambda | AbsPi
 
 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 prim_token =
+  | Numeral of Bigint.bigint (** representation of integer literals that appear in Coq scripts. *)
+  | String of string
 
 type raw_cases_pattern_expr =
   | RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t
   | 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 *)
+  (** [CPatCstr (_, c, l1, l2)] represents ((@c l1) l2) *)
   | RCPatAtom of Loc.t * Id.t option
   | RCPatOr of Loc.t * raw_cases_pattern_expr list
 
+type instance_expr = Misctypes.glob_level list
+
 type cases_pattern_expr =
   | CPatAlias of Loc.t * cases_pattern_expr * Id.t
   | CPatCstr of Loc.t * reference
-    * cases_pattern_expr list * cases_pattern_expr list
-  (** [CPatCstr (_, Inl c, l1, l2)] represents (@c l1) l2 *)
+    * cases_pattern_expr list option * cases_pattern_expr list
+  (** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *)
   | CPatAtom of Loc.t * reference option
   | CPatOr of Loc.t * cases_pattern_expr list
   | CPatNotation of Loc.t * notation * cases_pattern_notation_substitution
@@ -56,14 +60,13 @@ type 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
+  | CPatCast of Loc.t * cases_pattern_expr * constr_expr
 
 and cases_pattern_notation_substitution =
     cases_pattern_expr list *     (** for constr subterms *)
     cases_pattern_expr list list  (** for recursive notations *)
 
-type instance_expr = Misctypes.glob_level list
-
-type constr_expr =
+and constr_expr =
   | CRef of reference * instance_expr option
   | CFix of Loc.t * Id.t located * fix_expr list
   | CCoFix of Loc.t * Id.t located * cofix_expr list
@@ -73,9 +76,15 @@ type constr_expr =
   | CAppExpl of Loc.t * (proj_flag * reference * instance_expr option) * 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 *
-      case_expr list * branch_expr list
+  | CRecord of Loc.t * (reference * constr_expr) list
+
+  (* representation of the "let" and "match" constructs *)
+  | CCases of Loc.t                 (* position of the "match" keyword *)
+	      * case_style          (* determines whether this value represents "let" or "match" construct *)
+	      * constr_expr option  (* return-clause *)
+	      * case_expr list
+	      * branch_expr list    (* branches *)
+
   | CLetTuple of Loc.t * Name.t located list * (Name.t located option * constr_expr option) *
       constr_expr * constr_expr
   | CIf of Loc.t * constr_expr * (Name.t located option * constr_expr option)
@@ -90,8 +99,9 @@ type constr_expr =
   | CPrim of Loc.t * prim_token
   | CDelimiters of Loc.t * string * constr_expr
 
-and case_expr =
-  constr_expr * (Name.t located option * cases_pattern_expr option)
+and case_expr = constr_expr                 (* expression that is being matched *)
+	      * Name.t located option       (* as-clause *)
+	      * cases_pattern_expr option   (* in-clause *)
 
 and branch_expr =
   Loc.t * cases_pattern_expr list located list * constr_expr
@@ -115,13 +125,14 @@ and recursion_order_expr =
 and local_binder =
   | LocalRawDef of Name.t located * constr_expr
   | LocalRawAssum of Name.t located list * binder_kind * constr_expr
+  | LocalPattern of Loc.t * cases_pattern_expr * constr_expr option
 
 and constr_notation_substitution =
     constr_expr list *      (** for constr subterms *)
     constr_expr list list * (** for recursive notations *)
     local_binder list list (** for binders subexpressions *)
 
-type typeclass_constraint = Name.t located * binding_kind * constr_expr
+type typeclass_constraint = (Name.t located * Id.t located list option) * binding_kind * constr_expr
 
 and typeclass_context = typeclass_constraint list
 
-- 
cgit v1.2.3