From 69c27c774c444abf6260eda85de1cc1d54ade815 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 22 May 2000 19:54:58 +0000
Subject: Bugs d'index d'inductive

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@466 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/indrec.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'library')

diff --git a/library/indrec.ml b/library/indrec.ml
index e1609b25a..a8f708c45 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -228,13 +228,13 @@ let mis_make_indrec env sigma listdepkind mispec =
 		       | Some (_,Rel j) -> j 
 		       | _ -> assert false) in
 	    let indf = make_ind_family
-			 (mispec,rel_list (nrec+nbconstruct) nparams) in
+			 (mispeci,rel_list (nrec+nbconstruct) nparams) in
 	    let deftyi = 
 	      it_lambda_name env
 		(lambda_create env
 		   (build_dependent_inductive
 		      (lift_inductive_family nrec indf),
-		    mkMutCaseA (make_default_case_info mispec)
+		    mkMutCaseA (make_default_case_info mispeci)
                       (Rel (dect+j+1)) (Rel 1) branches))
 		(lift_context nrec lnames)
 	    in
-- 
cgit v1.2.3