- 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

1 files changed, 1 insertions, 1 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 *)