From a51f67a717a93cf61bfed79e70da9f35555dcab7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 1 Jul 2000 17:53:48 +0000
Subject: Précalcul de la forme canonique des constructeurs et arités pour
 traiter les cas du fichier Ensemble.v sans avoir à renormaliser à chaque fois

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

(limited to 'library')

diff --git a/library/impargs.ml b/library/impargs.ml
index 5b52f19760..bae96bc141 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -67,8 +67,8 @@ let inductives_table = ref Spmap.empty
 let declare_inductive_implicits sp =
   let mib = Global.lookup_mind sp in
   let imps_one_inductive mip =
-    (auto_implicits (body_of_type mip.mind_arity),
-     Array.map (fun c -> auto_implicits (body_of_type c)) mip.mind_lc)
+    (auto_implicits (mind_user_arity mip),
+     Array.map (fun c -> auto_implicits c) (mind_user_lc mip))
   in
   let imps = Array.map imps_one_inductive mib.mind_packets in
   inductives_table := Spmap.add sp imps !inductives_table
diff --git a/library/indrec.ml b/library/indrec.ml
index da5aeec345..d24ce2aa6a 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -52,7 +52,7 @@ let mis_make_case_com depopt env sigma mispec kind =
     if k = mis_nconstr mispec then
       let nbprod = k+1 in
       let ind = make_ind_family (mispec,rel_list nbprod nparams) in
-      let lnamesar,_ = get_arity env' sigma ind in
+      let lnamesar,_ = get_arity ind in
       let ci = make_default_case_info mispec in
       it_lambda_name env'
        	(lambda_create env'
@@ -69,7 +69,7 @@ let mis_make_case_com depopt env sigma mispec kind =
 	(add_branch (k+1))
   in
   let indf = make_ind_family (mispec,rel_list 0 nparams) in
-  let typP = make_arity env' sigma dep indf kind in
+  let typP = make_arity env' dep indf kind in
   it_lambda_name env (mkLambda_string "P" typP (add_branch 0)) lnamespar
     
 (* check if the type depends recursively on one of the inductive scheme *)
@@ -210,7 +210,7 @@ let mis_make_indrec env sigma listdepkind mispec =
             (* arity in the context P1..P_nrec f1..f_nbconstruct *)
 	    let params = rel_list (nrec+nbconstruct) nparams in
 	    let indf = make_ind_family (mispeci,params) in
-	    let lnames,_ = get_arity env sigma indf in
+	    let lnames,_ = get_arity indf in
 
 	    let nar = mis_nrealargs mispeci in
 	    let decf = nar+nrec+nbconstruct+nrec in 
@@ -281,7 +281,7 @@ let mis_make_indrec env sigma listdepkind mispec =
     let rec put_arity i = function 
       | (mispeci,dep,kinds)::rest -> 
 	  let indf = make_ind_family (mispeci,rel_list i nparams) in
-	  let typP = make_arity env sigma dep indf kinds in
+	  let typP = make_arity env dep indf kinds in
 	  mkLambda_string "P" typP (put_arity (i+1) rest)
       | [] -> 
 	  make_branch 0 listdepkind 
-- 
cgit v1.2.3