From 2f5c0f8880cd4ccc27cef4980768d35c9ebd26ea Mon Sep 17 00:00:00 2001
From: mohring
Date: Wed, 2 Nov 2005 22:12:16 +0000
Subject: Types inductifs parametriques

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/extraction.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'contrib/extraction')

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 0eb35e95b1..55ad52ee20 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -295,8 +295,8 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
     (* Everything concerning parameters. *)
     (* We do that first, since they are common to all the [mib]. *)
     let mip0 = mib.mind_packets.(0) in 
-    let npar = mip0.mind_nparams in
-    let epar = push_rel_context mip0.mind_params_ctxt env in
+    let npar = mib.mind_nparams in
+    let epar = push_rel_context mib.mind_params_ctxt env in
     (* First pass: we store inductive signatures together with *)
     (* their type var list. *)
     let packets = 
@@ -358,7 +358,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	  | _ -> []
 	in 
 	let field_names = 
-	  list_skipn mip0.mind_nparams (names_prod mip0.mind_user_lc.(0)) in 
+	  list_skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in 
 	assert (List.length field_names = List.length typ);
 	let projs = ref Cset.empty in 
 	let mp,d,_ = repr_kn kn in 
-- 
cgit v1.2.3