From e72024e2292a50684b7f280d6efb8fee090e2dbf Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 10 Sep 2000 20:37:37 +0000
Subject: Suppression de Abst

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

(limited to 'library')

diff --git a/library/indrec.ml b/library/indrec.ml
index c895787358..ddba73abed 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -56,10 +56,10 @@ let mis_make_case_com depopt env sigma mispec kind =
       it_lambda_name env'
        	(lambda_create env'
            (build_dependent_inductive ind,
-            mkMutCaseA ci
-	      (Rel (nbprod+nbargsprod))
-              (Rel 1)
-              (rel_vect nbargsprod k)))
+            mkMutCase (ci,
+		       Rel (nbprod+nbargsprod),
+		       Rel 1,
+		       rel_vect nbargsprod k)))
        	lnamesar
     else
       let cs = lift_constructor (k+1) constrs.(k) in
@@ -239,8 +239,8 @@ let mis_make_indrec env sigma listdepkind mispec =
 		(lambda_create env
 		   (build_dependent_inductive
 		      (lift_inductive_family nrec indf),
-		    mkMutCaseA (make_default_case_info mispeci)
-                      (Rel (dect+j+1)) (Rel 1) branches))
+		    mkMutCase (make_default_case_info mispeci,
+			       Rel (dect+j+1), Rel 1, branches)))
 		(lift_context nrec lnames)
 	    in
 	    let typtyi = 
-- 
cgit v1.2.3