From eb2862a2221276c44a90ed195d896c836674a66a Mon Sep 17 00:00:00 2001
From: barras
Date: Thu, 7 Feb 2002 16:11:03 +0000
Subject: 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
---
 kernel/indtypes.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 2221fc111e..746a942de9 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 *)
-- 
cgit v1.2.3