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.

11 files changed, 16 insertions, 30 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
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index 8eff327dcd..eaaf2dbb9f 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -75,7 +75,7 @@ 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
+  | CRecord of Loc.t * (reference * constr_expr) list
   | CCases of Loc.t * case_style * constr_expr option *
       case_expr list * branch_expr list
   | CLetTuple of Loc.t * Name.t located list * (Name.t located option * constr_expr option) *
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 2dec3b222a..440b368b95 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -224,10 +224,7 @@ GEXTEND Gram
       ] ]
   ;
   record_declaration:
-    [ [ fs = record_fields -> CRecord (!@loc, None, fs)
-(*       | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" -> *)
-(* 	  CRecord (!@loc, Some c, fs) *)
-    ] ]
+    [ [ fs = record_fields -> CRecord (!@loc, fs) ] ]
   ;
 
   record_fields:
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 7815a8f818..d1e1098259 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -752,10 +752,8 @@ let rec add_args id new_args b =
   | CCast(loc,b1,b2)  ->
       CCast(loc,add_args id new_args b1,
 	    Miscops.map_cast_type (add_args id new_args) b2)
-  | CRecord (loc, w, pars) ->
-      CRecord (loc,
-	       (match w with Some w -> Some (add_args id new_args w) | _ -> None),
-	       List.map (fun (e,o) -> e, add_args id new_args o) pars)
+  | CRecord (loc, pars) ->
+      CRecord (loc, List.map (fun (e,o) -> e, add_args id new_args o) pars)
   | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation")
   | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization")
   | CPrim _ -> b
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index c07057a096..3343997823 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -593,17 +593,9 @@ end) = struct
           return (p, lproj)
       | CApp (_,(None,a),l) ->
         return (pr_app (pr mt) a l, lapp)
-      | CRecord (_,w,l) ->
-        let beg =
-          match w with
-            | None ->
-              spc ()
-            | Some t ->
-              spc () ++ pr spc ltop t ++ spc ()
-              ++ keyword "with" ++ spc ()
-        in
+      | CRecord (_,l) ->
         return (
-          hv 0 (str"{|" ++ beg ++
+          hv 0 (str"{|" ++ spc () ++
                   prlist_with_sep pr_semicolon
                   (fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr spc ltop c)) l
                 ++ str" |}"),
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index b18e35a472..70eccc2403 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -457,7 +457,7 @@ and pp_expr ?(attr=[]) e =
           (return @
            [Element ("scrutinees", [], List.map pp_case_expr cel)] @
            [pp_branch_expr_list bel]))
-  | CRecord (_, _, _) -> assert false
+  | CRecord (_, _) -> assert false
   | CLetIn (loc, (varloc, var), value, body) ->
       xmlApply loc
         (xmlOperator "let" loc ::
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 2dfebc9a3c..eddefb2799 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1710,7 +1710,7 @@ let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
 let anew_instance global binders instance fields =
   new_instance (Flags.is_universe_polymorphism ()) 
-    binders instance (Some (true, CRecord (Loc.ghost,None,fields)))
+    binders instance (Some (true, CRecord (Loc.ghost,fields)))
     ~global ~generalize:false None
 
 let declare_instance_refl global binders a aeq n lemma =
@@ -1925,7 +1925,7 @@ let add_morphism glob binders m s n =
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
     ignore(new_instance ~global:glob poly binders instance 
-	     (Some (true, CRecord (Loc.ghost,None,[])))
+	     (Some (true, CRecord (Loc.ghost,[])))
 	      ~generalize:false ~tac ~hook:(declare_projection n instance_id) None)
 
 (** Bind to "rewrite" too *)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index ab18350c5c..86b4712326 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -195,7 +195,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
     else (
       let props =
 	match props with
-	| Some (true, CRecord (loc, _, fs)) ->
+	| Some (true, CRecord (loc, fs)) ->
 	    if List.length fs > List.length k.cl_props then
 	      mismatched_props env' (List.map snd fs) k.cl_props;
 	    Some (Inl fs)