Bug env vis à vis du let in

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

1 files changed, 5 insertions, 4 deletions

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 22eba722c..270742601 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -20,7 +20,8 @@ let rec subst_type env sigma typ = function
   | [] -> typ
   | h::rest ->
       match kind_of_term (whd_betadeltaiota env sigma typ) with
-          IsProd (_,c1,c2) -> subst_type env sigma (subst1 h c2) rest
+        | IsProd (na,c1,c2) -> 
+	    subst_type (push_rel_assum (na,c1) env) sigma (subst1 h c2) rest
         | _ -> anomaly "Non-functional construction"
 
 (* Si ft est le type d'un terme f, lequel est appliqué à args, *)
@@ -29,12 +30,12 @@ let rec subst_type env sigma typ = function
 (* et sinon on substitue *)
 
 let sort_of_atomic_type env sigma ft args =
-  let rec concl_of_arity ar =
+  let rec concl_of_arity env ar =
     match kind_of_term (whd_betadeltaiota env sigma ar) with
-      | IsProd (_, _, b) -> concl_of_arity b
+      | IsProd (na, t, b) -> concl_of_arity (push_rel_assum (na,t) env) b
       | IsSort s -> s
       | _ -> outsort env sigma (subst_type env sigma ft (Array.to_list args))
-  in concl_of_arity ft
+  in concl_of_arity env ft
 
 let typeur sigma metamap =
 let rec type_of env cstr=