From f1b471d931368cb0d0a322e684a0e4b217478a3f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 8 Mar 2015 16:37:58 +0100
Subject: Fixing bug #2951.

---
 toplevel/record.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/toplevel/record.ml b/toplevel/record.ml
index 55f533512b..737b7fb59f 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -472,10 +472,15 @@ 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
+    | (_, Some _, _) -> None
+    | (_, None, t) -> Some (lazy t)
+    in
+    let args = List.map_filter map ctx in
     let ty = Inductive.type_of_inductive_knowing_parameters
       (push_rel_context ctx (Global.env ()))
       ((mind,oneind),inst)
-      (Array.map (fun x -> lazy x) (Termops.extended_rel_vect 0 ctx))
+      (Array.of_list args)
     in
       { cl_impl = IndRef ind;
 	cl_context = List.map (const None) ctx, ctx;
-- 
cgit v1.2.3