From 25ea09274a8b085092963fcccf0400f8826f5544 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 8 Nov 2001 14:10:21 +0000
Subject: Rétablissement de la persistance des Cast; typage des LetIn sans
 recours à Cast

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2171 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/typing.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 7dd552e383..b36c032046 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -111,10 +111,13 @@ let rec execute mf env sigma cstr =
 	j
 
      | LetIn (name,c1,c2,c3) ->
-        let j1 = execute mf env sigma (mkCast (c1, c2)) in
-        let env1 = push_rel (name,Some j1.uj_val,j1.uj_type) env in
+        let j1 = execute mf env sigma c1 in
+        let j2 = execute mf env sigma c2 in
+        let j2 = type_judgment env sigma j2 in
+        let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in
         let j3 = execute mf env1 sigma c3 in
-        judge_of_letin env name j1 j3
+        let (j,_) = judge_of_letin env name j1 j2 j3 in
+        j
   
     | Cast (c,t) ->
         let cj = execute mf env sigma c in
-- 
cgit v1.2.3