Plus de env et sigma dans get_arity, plus de sigma dans make_arity

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@546 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 7 insertions, 7 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c4dd055531..47fcdcc159 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -85,7 +85,7 @@ let make_case_ml isrec pred c ci lf =
  * where A'_bar = A_bar[p_bar <- globargs] *)
 
 let build_notdep_pred env sigma indf pred =
-  let arsign,_ = get_arity env sigma indf in
+  let arsign,_ = get_arity indf in
   let nar = List.length arsign in
   it_lambda_name env (lift nar pred) arsign
 
@@ -549,7 +549,7 @@ let infer_predicate env isevars typs cstrs (IndFamily (mis,_) as indf) =
 
   (* First strategy: no dependencies at all *)
   let (cclargs,_,typn) = eqns.(mis_nconstr mis -1) in
-  let (sign,_) = get_arity env !isevars indf in
+  let (sign,_) = get_arity indf in
   if array_for_all (fun (_,_,typ) -> the_conv_x env isevars typn typ) eqns
   then
     let pred = lam_it (lift (List.length sign) typn) sign in
@@ -621,7 +621,7 @@ let rec extract_predicate = function
 let abstract_predicate env sigma indf = function
   | PrProd _ | PrCcl _ -> anomaly "abstract_predicate: must be some LetIn"
   | PrLetIn ((_,copt),pred) ->
-      let asign,_ = get_arity env sigma indf in
+      let asign,_ = get_arity indf in
       let sign =
 	List.map (fun (na,t) -> (named_hd (Global.env()) t na,t)) asign in
       let dep = copt<> None in
@@ -895,7 +895,7 @@ let coerce_row typing_fun isevars env row tomatch =
 	     let indtyp = inh_coerce_to_ind isevars env typ tyi in
 	     IsInd (typ,find_rectype env !isevars typ)
 	   with NotCoercible ->
-	     (* 2 cas : pas le bon inductive ou pas un inductif du tout *)
+	     (* 2 cases : Not the right inductive or not an inductive at all *)
 	     try
 	       let mind,_ = find_mrectype env !isevars typ in
 	       error_bad_constructor_loc cloc CCI
@@ -921,7 +921,7 @@ let build_expected_arity env isevars isdep tomatchl =
   let cook n = function
     | _,IsInd (_,IndType(indf,_)) ->
 	let indf' = lift_inductive_family n indf in
-	(build_dependent_inductive indf', fst (get_arity env !isevars indf'))
+	(build_dependent_inductive indf', fst (get_arity indf'))
     | _,NotInd _ -> anomaly "Should have been catched in case_dependent"
   in
   let rec buildrec n = function
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 41b9d10695..efbf7594a8 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -75,7 +75,7 @@ let transform_rec loc env sigma (p,c,lf) (indt,pt) =
     let depFvec = Array.init (mis_ntypes mispec) init_depFvec in
     let constrs = get_constructors indf in
     (* build now the fixpoint *)
-    let lnames,_ = get_arity env sigma indf in
+    let lnames,_ = get_arity indf in
     let nar = List.length lnames in
     let nparams = mis_nparams mispec in
     let ci = make_default_case_info mispec in
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 535a0c5836..72cd94c1dc 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -54,7 +54,7 @@ let rec type_of env cstr=
         let IndType (indf,realargs) =
           try find_rectype env sigma (type_of env c)
           with Induc -> anomaly "type_of: Bad recursive type" in
-	let (aritysign,_) = get_arity env sigma indf in
+	let (aritysign,_) = get_arity indf in
 	let (psign,_) = splay_prod env sigma (type_of env p) in
         let al =
 	  if List.length psign > List.length aritysign