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

6 files changed, 13 insertions, 13 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
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 02e35d4f2d..22bc94b691 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -462,7 +462,7 @@ let descend_then sigma env head dirn =
   (dirn_nlams,
    dirn_env,
    (fun dirnval (dfltval,resty) ->
-      let aritysign,_ = get_arity env sigma indf in
+      let aritysign,_ = get_arity indf in
       let p = lam_it (lift (mis_nrealargs mispec) resty) aritysign in
       let build_branch i =
 	let result = if i = dirn then dirnval else dfltval in
@@ -500,7 +500,7 @@ let construct_discriminator sigma env dirn c sort =
       errorlabstrm "Equality.construct_discriminator"
 	[< 'sTR "Cannot discriminate on inductive constructors with 
 		 dependent types" >] in
-  let arsign,arsort = get_arity env sigma indf in
+  let arsign,arsort = get_arity indf in
   let (true_0,false_0,sort_0) = 
     match necessary_elimination arsort (destSort sort) with
       | Type_Type -> build_UnitT (), build_EmptyT (), (Type dummy_univ)
@@ -524,7 +524,7 @@ let rec build_discriminator sigma env dirn c sort = function
       let cty = type_of env sigma c in
       let IndType (indf,_) =
 	try find_rectype env sigma cty with Not_found -> assert false in
-      let _,arsort = get_arity env sigma indf in
+      let _,arsort = get_arity indf in
       let nparams = mis_nparams (fst (dest_ind_family indf)) in
       let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in
       let newc = Rel(cnum_nlams-(argnum-nparams)) in
diff --git a/tactics/inv.ml b/tactics/inv.ml
index d7de3df9be..385cd574cd 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -93,7 +93,7 @@ let make_inv_predicate env sigma ind id status concl =
     match status with
       | NoDep ->
 	  (* We push the arity and leave concl unchanged *)
-	  let hyps_arity,_ = get_arity env sigma indf in
+	  let hyps_arity,_ = get_arity indf in
 	  let env' = push_rels hyps_arity env in
 	  (hyps_arity,concl)
       | Dep dflt_concl ->
@@ -108,7 +108,7 @@ let make_inv_predicate env sigma ind id status concl =
               | Some concl -> concl (*assumed it's some [x1..xn,H:I(x1..xn)]C*)
               | None ->
 		let sort = get_sort_of env sigma concl in
-		let p = make_arity env sigma true indf sort in
+		let p = make_arity env true indf sort in
 		abstract_list_all env sigma p concl (realargs@[VAR id])
 	  in
 	  let hyps,_ = decompose_lam pred in
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 281c1eb189..60a4cd3647 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -149,7 +149,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
   let p = next_ident_away (id_of_string "P") allvars in
   let pty,goal =
     if dep_option  then
-      let pty = make_arity env sigma true indf sort in
+      let pty = make_arity env true indf sort in
       let goal = 
 	mkProd Anonymous (mkAppliedInd ind) (applist(VAR p,realargs@[Rel 1]))
       in