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

3 files changed, 18 insertions, 15 deletions

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index a2c6fe686f..e99673fe1a 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -156,12 +156,10 @@ let judge_of_abstraction env name var j =
 
 (* Type of let-in. *)
 
-let judge_of_letin env name defj j =
-  let v = match kind_of_term defj.uj_val with
-      Cast(c,t) -> c
-    | _ -> defj.uj_val in
-  { uj_val = mkLetIn (name, v, defj.uj_type, j.uj_val) ;
-    uj_type = type_app (subst1 v) j.uj_type }
+let judge_of_letin env name defj typj j =
+  let cst = conv_leq env defj.uj_type typj.utj_val in
+  { uj_val = mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val) ;
+    uj_type = type_app (subst1 defj.uj_val) j.uj_type }, cst
 
 (* Type of an application. *)
 
@@ -237,7 +235,7 @@ let judge_of_product env name t1 t2 =
 let judge_of_cast env cj tj =
   try 
     let cst = conv_leq env cj.uj_type tj.utj_val in
-    { uj_val = j_val cj;
+    { uj_val = mkCast (j_val cj, tj.utj_val);
       uj_type = tj.utj_val },
     cst
   with NotConvertible ->
@@ -373,10 +371,12 @@ let rec execute env cstr cu =
           (judge_of_product env name varj varj')
 
     | LetIn (name,c1,c2,c3) ->
-        let (j,cu1) = execute env (mkCast(c1,c2)) cu in
-        let env1 = push_rel (name,Some j.uj_val,j.uj_type) env in
+        let (j1,cu1) = execute env c1 cu in
+        let (j2,cu2) = execute_type env c2 cu in
+        let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in
         let (j',cu2) = execute env1 c3 cu1 in
-        (judge_of_letin env name j j', cu2)
+        univ_combinator cu2
+          (judge_of_letin env name j1 j2 j')
 	  
     | Cast (c,t) ->
         let (cj,cu1) = execute env c cu in
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 24ffa47b12..1605328cb4 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -68,8 +68,8 @@ val judge_of_product :
 
 (* s Type of a let in. *)
 val judge_of_letin :
-  env -> name -> unsafe_judgment -> unsafe_judgment 
-    -> unsafe_judgment
+  env -> name -> unsafe_judgment -> unsafe_type_judgment -> unsafe_judgment 
+    -> unsafe_judgment * constraints
 
 (*s Type of a cast. *)
 val judge_of_cast :
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