CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified

9 files changed, 47 insertions, 45 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 2d48ea4d07..161fd1eb1d 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -178,7 +178,7 @@ and args_eq (a1,e1) (a2,e2) =
   Option.equal (eq_located explicitation_eq) e1 e2 &&
   constr_expr_eq a1 a2
 
-and case_expr_eq (e1, (n1, p1)) (e2, (n2, p2)) =
+and case_expr_eq (e1, n1, p1) (e2, n2, p2) =
   constr_expr_eq e1 e2 &&
   Option.equal (eq_located Name.equal) n1 n2 &&
   Option.equal cases_pattern_expr_eq p1 p2
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index ba20f9fa06..ed85c38de0 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -721,26 +721,29 @@ let rec extern inctx scopes vars r =
 	(cases_predicate_names tml) vars in
     let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in
     let tml = List.map (fun (tm,(na,x)) ->
-      let na' = match na,tm with
-        | Anonymous, GVar (_, id) ->
-            begin match rtntypopt with
-            | None -> None
-            | Some ntn ->
-              if occur_glob_constr id ntn then
-                Some (Loc.ghost, Anonymous)
-              else None
-            end
-        | Anonymous, _ -> None
-        | Name id, GVar (_,id') when Id.equal id id' -> None
-        | Name _, _ -> Some (Loc.ghost,na) in
-      (sub_extern false scopes vars tm,
-       (na',Option.map (fun (loc,ind,nal) ->
-	 let args = List.map (fun x -> PatVar (Loc.ghost, x)) nal in
-	 let fullargs =
-	   if !Flags.in_debugger then args else
-	     Notation_ops.add_patterns_for_params ind args in
-	 extern_ind_pattern_in_scope scopes vars ind fullargs
-	) x))) tml in
+                 let na' = match na,tm with
+                   | Anonymous, GVar (_, id) ->
+                      begin match rtntypopt with
+                            | None -> None
+                            | Some ntn ->
+                               if occur_glob_constr id ntn then
+                                 Some (Loc.ghost, Anonymous)
+                               else None
+                      end
+                   | Anonymous, _ -> None
+                   | Name id, GVar (_,id') when Id.equal id id' -> None
+                   | Name _, _ -> Some (Loc.ghost,na) in
+                 (sub_extern false scopes vars tm,
+                  na',
+                  Option.map (fun (loc,ind,nal) ->
+                              let args = List.map (fun x -> PatVar (Loc.ghost, x)) nal in
+                              let fullargs =
+                                if !Flags.in_debugger then args else
+                                  Notation_ops.add_patterns_for_params ind args in
+                              extern_ind_pattern_in_scope scopes vars ind fullargs
+                             ) x))
+                tml
+    in
     let eqns = List.map (extern_eqn inctx scopes vars) eqns in
     CCases (loc,sty,rtntypopt',tml,eqns)
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8afe630ec5..8a86d30220 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1506,7 +1506,7 @@ let internalize globalenv env allow_patvar lvar c =
 	  intern env app
 	end
     | CCases (loc, sty, rtnpo, tms, eqns) ->
-      let as_in_vars = List.fold_left (fun acc (_,(na,inb)) ->
+      let as_in_vars = List.fold_left (fun acc (_,na,inb) ->
 	Option.fold_left (fun x tt -> List.fold_right Id.Set.add (ids_of_cases_indtype tt) x)
 	  (Option.fold_left (fun x (_,y) -> match y with | Name y' -> Id.Set.add y' x |_ -> x) acc na)
 	  inb) Id.Set.empty tms in
@@ -1542,7 +1542,7 @@ let internalize globalenv env allow_patvar lvar c =
     | CLetTuple (loc, nal, (na,po), b, c) ->
 	let env' = reset_tmp_scope env in
 	(* "in" is None so no match to add *)
-        let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,(na,None)) in
+        let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in
         let p' = Option.map (fun u ->
 	  let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
 	    (Loc.ghost,na') in
@@ -1551,7 +1551,7 @@ let internalize globalenv env allow_patvar lvar c =
                    intern (List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
     | CIf (loc, c, (na,po), b1, b2) ->
       let env' = reset_tmp_scope env in
-      let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,(na,None)) in (* no "in" no match to ad too *)
+      let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,na,None) in (* no "in" no match to ad too *)
       let p' = Option.map (fun p ->
           let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env)
 	    (Loc.ghost,na') in
@@ -1628,7 +1628,7 @@ let internalize globalenv env allow_patvar lvar c =
       let rhs' = intern {env with ids = env_ids} rhs in
       (loc,eqn_ids,pl,rhs')) pll
 
-  and intern_case_item env forbidden_names_for_gen (tm,(na,t)) =
+  and intern_case_item env forbidden_names_for_gen (tm,na,t) =
     (*the "match" part *)
     let tm' = intern env tm in
     (* the "as" part *)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 1231f11555..15ac46e29e 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -51,7 +51,7 @@ let ids_of_cases_indtype =
 
 let ids_of_cases_tomatch tms =
   List.fold_right
-    (fun (_,(ona,indnal)) l ->
+    (fun (_,ona,indnal) l ->
       Option.fold_right (fun t -> (@) (ids_of_cases_indtype t))
       indnal (Option.fold_right (Loc.down_located name_cons) ona l))
     tms []
@@ -120,7 +120,7 @@ let fold_constr_expr_with_binders g f n acc = function
   | CCases (loc,sty,rtnpo,al,bl) ->
       let ids = ids_of_cases_tomatch al in
       let acc = Option.fold_left (f (List.fold_right g ids n)) acc rtnpo in
-      let acc = List.fold_left (f n) acc (List.map fst al) in
+      let acc = List.fold_left (f n) acc (List.map (fun (fst,_,_) -> fst) al) in
       List.fold_right (fun (loc,patl,rhs) acc ->
 	let ids = ids_of_pattern_list patl in
 	f (Id.Set.fold g ids n) acc rhs) bl acc
@@ -224,7 +224,7 @@ let map_constr_expr_with_binders g f e = function
       let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in
       let ids = ids_of_cases_tomatch a in
       let po = Option.map (f (List.fold_right g ids e)) rtnpo in
-      CCases (loc, sty, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl)
+      CCases (loc, sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl)
   | CLetTuple (loc,nal,(ona,po),b,c) ->
       let e' = List.fold_right (Loc.down_located (name_fold g)) nal e in
       let e'' = Option.fold_right (Loc.down_located (name_fold g)) ona e in
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index 6543db6a17..8eff327dcd 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -93,7 +93,7 @@ type constr_expr =
   | CDelimiters of Loc.t * string * constr_expr
 
 and case_expr =
-  constr_expr * (Name.t located option * cases_pattern_expr option)
+  constr_expr * Name.t located option * cases_pattern_expr option
 
 and branch_expr =
   Loc.t * cases_pattern_expr list located list * constr_expr
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 8df91da24b..2dec3b222a 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -267,14 +267,14 @@ GEXTEND Gram
           CLetTuple (!@loc,lb,po,c1,c2)
       | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
           "in"; c2 = operconstr LEVEL "200" ->
-	    CCases (!@loc, LetPatternStyle, None, [(c1,(None,None))], [(!@loc, [(!@loc,[p])], c2)])
+	    CCases (!@loc, LetPatternStyle, None, [c1, None, None], [(!@loc, [(!@loc,[p])], c2)])
       | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
 	  rt = case_type; "in"; c2 = operconstr LEVEL "200" ->
-	    CCases (!@loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, None))], [(!@loc, [(!@loc, [p])], c2)])
+	    CCases (!@loc, LetPatternStyle, Some rt, [c1, aliasvar p, None], [(!@loc, [(!@loc, [p])], c2)])
       | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200";
 	  ":="; c1 = operconstr LEVEL "200"; rt = case_type;
           "in"; c2 = operconstr LEVEL "200" ->
-	    CCases (!@loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, Some t))], [(!@loc, [(!@loc, [p])], c2)])
+	    CCases (!@loc, LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [(!@loc, [(!@loc, [p])], c2)])
       | "if"; c=operconstr LEVEL "200"; po = return_type;
 	"then"; b1=operconstr LEVEL "200";
         "else"; b2=operconstr LEVEL "200" ->
@@ -338,11 +338,10 @@ GEXTEND Gram
         br=branches; "end" -> CCases(!@loc,RegularStyle,ty,ci,br) ] ]
   ;
   case_item:
-    [ [ c=operconstr LEVEL "100"; p=pred_pattern -> (c,p) ] ]
-  ;
-  pred_pattern:
-    [ [ ona = OPT ["as"; id=name -> id];
-        ty = OPT ["in"; t=pattern -> t] -> (ona,ty) ] ]
+    [ [ c=operconstr LEVEL "100";
+        ona = OPT ["as"; id=name -> id];
+	ty = OPT ["in"; t=pattern -> t] ->
+	   (c,ona,ty) ] ]
   ;
   case_type:
     [ [ "return"; ty = operconstr LEVEL "100" -> ty ] ]
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index bf9da870e4..7815a8f818 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -728,9 +728,9 @@ let rec add_args id new_args b =
 	   List.map (fun (e,o) -> add_args id new_args e,o) bl)
   | CCases(loc,sty,b_option,cel,cal) ->
       CCases(loc,sty,Option.map (add_args id new_args) b_option,
-	     List.map (fun (b,(na,b_option)) ->
+	     List.map (fun (b,na,b_option) ->
 			 add_args id new_args b,
-			 (na, b_option)) cel,
+			 na, b_option) cel,
 	     List.map (fun (loc,cpl,e) -> (loc,cpl,add_args id new_args e)) cal
 	    )
   | CLetTuple(loc,nal,(na,b_option),b1,b2) ->
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 663b8b8101..56429410cb 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -457,7 +457,7 @@ end) = struct
         (pr_decl true) dl ++
         fnl() ++ keyword "for" ++ spc () ++ pr_id id
 
-  let pr_asin pr (na,indnalopt) =
+  let pr_asin pr na indnalopt =
     (match na with (* Decision of printing "_" or not moved to constrextern.ml *)
       | Some na -> spc () ++ keyword "as" ++ spc () ++  pr_lname na
       | None -> mt ()) ++
@@ -465,8 +465,8 @@ end) = struct
         | None -> mt ()
         | Some t -> spc () ++ keyword "in" ++ spc () ++ pr_patt lsimplepatt t)
 
-  let pr_case_item pr (tm,asin) =
-    hov 0 (pr (lcast,E) tm ++ pr_asin pr asin)
+  let pr_case_item pr (tm,as_clause, in_clause) =
+    hov 0 (pr (lcast,E) tm ++ pr_asin pr as_clause in_clause)
 
   let pr_case_type pr po =
     match po with
@@ -611,12 +611,12 @@ end) = struct
                 ++ str" |}"),
           latom
         )
-      | CCases (_,LetPatternStyle,rtntypopt,[c,asin],[(_,[(loc,[p])],b)]) ->
+      | CCases (_,LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,[(loc,[p])],b)]) ->
         return (
           hv 0 (
             keyword "let" ++ spc () ++ str"'" ++
               hov 0 (pr_patt ltop p ++
-                       pr_asin (pr_dangling_with_for mt pr) asin ++
+                       pr_asin (pr_dangling_with_for mt pr) as_clause in_clause ++
                        str " :=" ++ pr spc ltop c ++
                        pr_case_type (pr_dangling_with_for mt pr) rtntypopt ++
                        spc () ++ keyword "in" ++ pr spc ltop b)),
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index 2a09143940..1996d35259 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -347,7 +347,7 @@ and pp_cases_pattern_expr cpe =
       xmlApply loc
         (xmlOperator "delimiter" ~attr:["name", delim] loc ::
           [pp_cases_pattern_expr cpe])
-and pp_case_expr (e, (name, pat)) =
+and pp_case_expr (e, name, pat) =
   match name, pat with
   | None, None -> xmlScrutinee [pp_expr e]
   | Some (loc, name), None ->