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

4 files changed, 31 insertions, 28 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 2d48ea4d0..161fd1eb1 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 ba20f9fa0..ed85c38de 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 8afe630ec..8a86d3022 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 1231f1155..15ac46e29 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