erreur mineure dans le test des inductifs imbriques

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

1 files changed, 3 insertions, 1 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 2221fc111..746a942de 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -397,7 +397,9 @@ let check_positivity env ntypes hyps nparams i indlc =
     let auxlcvect = abstract_mind_lc env auxntyp auxnpar auxlc in
     (* Extends the environment with a variable corresponding to
        the inductive def *)
-    let env' = push_rel (Anonymous,None,type_of_inductive env mi) env in
+    let env' =
+      push_rel (Anonymous,None,
+                hnf_prod_applist env (type_of_inductive env mi) lpar) env in
     let newidx = n + auxntyp in
     let _ = 
       (* fails if the inductive type occurs non positively *)