From a1aff01d16bad2f44392fd5cb804092e12e558ed Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Wed, 16 Dec 2015 16:19:51 +0100
Subject: 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.
---
 plugins/funind/indfun.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'plugins')

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
-- 
cgit v1.2.3