decast must also perform LetIn reduction now.

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 28089b4cc059ea9bfdbe929adeb755cef2198721..c86a27ad04e89c3424ebff3b5c7ed8f8cd6be9e6 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1183,10 +1183,12 @@ and type_of t =
         let (_,ty,_) = List.nth fl i in
          ty
 
+ (* CSC: wrong name and position: decast really does Cast-LetIn reduction *)
  and decast =
   let module C = Cic in
    function
-      C.Cast (t,_) -> t
+      C.Cast (t,_) -> decast t
+    | C.LetIn (_,s,t) -> decast (CicSubstitution.subst s t)
     | t -> t
 
  and sort_of_prod (t1, t2) =
@@ -1196,7 +1198,10 @@ and type_of t =
         when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
          C.Sort s2
     | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
-    | (_,_) -> raise (NotWellTyped "Prod")
+    | (_,_) ->
+      raise
+       (NotWellTyped ("Prod: sort1= " ^ CicPp.ppterm t1 ^ " ;
+         sort2= " ^ CicPp.ppterm t2))
 
  and eat_prods hetype =
   (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)