- Indtypes: en attente opinion CoRN, les occurrences de Type non explicites

  (i.e. cachées sous un nom de constante) sont considérées comme
  monomorphes.
- Divers: renommage type_of_applied_inductive, un peu de documentation.


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

4 files changed, 9 insertions, 9 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 01841641c..d1d30980b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -415,7 +415,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  match kind_of_term resj.uj_val with
 	  | App (f,args) when isInd f ->
 	      let sigma = evars_of !isevars in
-	      let t = Retyping.type_of_applied_inductive env sigma (destInd f) args in
+	      let t = Retyping.type_of_inductive_knowing_parameters env sigma (destInd f) args in
 	      let s = snd (splay_arity env sigma t) in
 	      on_judgment_type (set_inductive_level env s) resj
 		(* Rem: no need to send sigma: no head evar, it's an arity *)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 2fdb4148a..1756c8377 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -74,7 +74,7 @@ let typeur sigma metamap =
     | Fix ((_,i),(_,tys,_)) -> tys.(i)
     | CoFix (i,(_,tys,_)) -> tys.(i)
     | App(f,args) when isInd f ->
-	let t = type_of_applied_inductive env (destInd f) args in
+	let t = type_of_inductive_knowing_parameters env (destInd f) args in
         strip_outer_cast (subst_type env sigma t (Array.to_list args))
     | App(f,args) ->
         strip_outer_cast
@@ -98,7 +98,7 @@ let typeur sigma metamap =
 	  | Prop Null, (Type _ as s) -> s
 	  | Type u1, Type u2 -> Type (Univ.sup u1 u2))
     | App(f,args) when isInd f ->
-	let t = type_of_applied_inductive env (destInd f) args in
+	let t = type_of_inductive_knowing_parameters env (destInd f) args in
         sort_of_atomic_type env sigma t args
     | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
     | Lambda _ | Fix _ | Construct _ ->
@@ -117,17 +117,17 @@ let typeur sigma metamap =
         anomaly "sort_of: Not a type (1)"
     | _ -> family_of_sort (decomp_sort env sigma (type_of env t))
 
-  and type_of_applied_inductive env ind args =
+  and type_of_inductive_knowing_parameters env ind args =
     let (_,mip) = lookup_mind_specif env ind in
     let argtyps = Array.map (fun c -> nf_evar sigma (type_of env c)) args in
-    Inductive.type_of_applied_inductive env mip argtyps
+    Inductive.type_of_inductive_knowing_parameters env mip argtyps
 
-  in type_of, sort_of, sort_family_of, type_of_applied_inductive
+  in type_of, sort_of, sort_family_of, type_of_inductive_knowing_parameters
 
 let get_type_of env sigma c = let f,_,_,_ = typeur sigma [] in f env c
 let get_sort_of env sigma t = let _,f,_,_ = typeur sigma [] in f env t
 let get_sort_family_of env sigma c = let _,_,f,_ = typeur sigma [] in f env c
-let type_of_applied_inductive env sigma ind args =
+let type_of_inductive_knowing_parameters env sigma ind args =
   let _,_,_,f = typeur sigma [] in f env ind args
 
 let get_type_of_with_meta env sigma metamap = 
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 8631f5545..900a96829 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -34,5 +34,5 @@ val get_assumption_of : env -> evar_map -> constr -> types
 (* Makes an unsafe judgment from a constr *)
 val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment
 
-val type_of_applied_inductive : env -> evar_map -> inductive -> 
+val type_of_inductive_knowing_parameters : env -> evar_map -> inductive -> 
   constr array -> types
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 8e10b0aff..57c83fa7e 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -92,7 +92,7 @@ let rec execute env evd cstr =
 	let j =
 	if isInd f then
 	  (* Sort-polymorphism of inductive types *)
-	  judge_of_applied_inductive env (destInd f)
+	  judge_of_inductive_knowing_parameters env (destInd f)
 	    (jv_nf_evar (evars_of evd) jl)
 	else
 	  execute env evd f