From b3a57e84241c40915169aa410f5606175cf609be Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 29 Oct 2016 14:38:06 +0200
Subject: Removing dead code.

---
 toplevel/record.ml | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/toplevel/record.ml b/toplevel/record.ml
index 9c4d41ea50..ba9e7ee22f 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -517,10 +517,6 @@ let add_inductive_class ind =
   let k =
     let ctx = oneind.mind_arity_ctxt in
     let inst = Univ.UContext.instance mind.mind_universes in
-    let map = function
-    | LocalDef _ -> None
-    | LocalAssum (_, t) -> Some (lazy t)
-    in
     let ty = Inductive.type_of_inductive
       (push_rel_context ctx (Global.env ()))
       ((mind,oneind),inst)
-- 
cgit v1.2.3