CLEANUP: removing unused field

I have removed the second field of the "Constrexpr.CRecord" variant
because once it was set to "None"
it never changed to anything else.
It was just carried and copied around.

4 files changed, 6 insertions, 7 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 161fd1eb1d..a97e8e6db7 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -125,11 +125,10 @@ let rec constr_expr_eq e1 e2 =
       Option.equal Int.equal proj1 proj2 &&
       constr_expr_eq e1 e2 &&
       List.equal args_eq al1 al2
-  | CRecord (_, e1, l1), CRecord (_, e2, l2) ->
+  | CRecord (_, l1), CRecord (_, l2) ->
     let field_eq (r1, e1) (r2, e2) =
       eq_reference r1 r2 && constr_expr_eq e1 e2
     in
-    Option.equal constr_expr_eq e1 e2 &&
     List.equal field_eq l1 l2
   | CCases(_,_,r1,a1,brl1), CCases(_,_,r2,a2,brl2) ->
       (** Don't care about the case_style *)
@@ -238,7 +237,7 @@ let constr_loc = function
   | CLetIn (loc,_,_,_) -> loc
   | CAppExpl (loc,_,_) -> loc
   | CApp (loc,_,_) -> loc
-  | CRecord (loc,_,_) -> loc
+  | CRecord (loc,_) -> loc
   | CCases (loc,_,_,_,_) -> loc
   | CLetTuple (loc,_,_,_,_) -> loc
   | CIf (loc,_,_,_,_) -> loc
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 5c9e80df3d..af2206d968 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -680,7 +680,7 @@ let rec extern inctx scopes vars r =
 				 | head :: tail -> ip q locs' tail
 				     ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc)
 		   in
-		 CRecord (loc, None, List.rev (ip projs locals args []))
+		 CRecord (loc, List.rev (ip projs locals args []))
 	       with
 		 | Not_found | No_match | Exit ->
 		     extern_app loc inctx
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 68bc0b1092..c0203b0666 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1479,7 +1479,7 @@ let internalize globalenv env allow_patvar lvar c =
           apply_impargs c env impargs args_scopes 
 	    (merge_impargs l args) loc
 
-    | CRecord (loc, _, fs) ->
+    | CRecord (loc, fs) ->
 	let cargs =
 	  sort_fields true loc fs
 	    (fun k l -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true)), Misctypes.IntroAnonymous, None) :: l)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 15ac46e29e..837630183e 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -116,7 +116,7 @@ let fold_constr_expr_with_binders g f n acc = function
   | CDelimiters (loc,_,a) -> f n acc a
   | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ ->
       acc
-  | CRecord (loc,_,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l
+  | CRecord (loc,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l
   | 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
@@ -218,7 +218,7 @@ let map_constr_expr_with_binders g f e = function
   | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
   | CHole _ | CEvar _ | CPatVar _ | CSort _
   | CPrim _ | CRef _ as x -> x
-  | CRecord (loc,p,l) -> CRecord (loc,p,List.map (fun (id, c) -> (id, f e c)) l)
+  | CRecord (loc,l) -> CRecord (loc,List.map (fun (id, c) -> (id, f e c)) l)
   | CCases (loc,sty,rtnpo,a,bl) ->
       (* TODO: apply g on the binding variables in pat... *)
       let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in