From 8bb6ef3137ce036fdb6f0f6b3debf4a7e4e30f09 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 18 Dec 2001 09:32:07 +0000
Subject: Grossière erreur de typage

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2305 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/retyping.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index da12c6449c..c2f42b34e7 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -29,8 +29,7 @@ let rec subst_type env sigma typ = function
   | [] -> typ
   | h::rest ->
       match kind_of_term (whd_betadeltaiota env sigma typ) with
-        | Prod (na,c1,c2) -> 
-	    subst_type (push_rel (na,None,c1) env) sigma (subst1 h c2) rest
+        | Prod (na,c1,c2) -> subst_type env sigma (subst1 h c2) rest
         | _ -> anomaly "Non-functional construction"
 
 (* Si ft est le type d'un terme f, lequel est appliqué à args, *)
-- 
cgit v1.2.3