From c748674f4d7e3dc104d3edb0c31bc3c006a455f9 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 4 Dec 2001 09:19:20 +0000 Subject: [PATCH] decast must also perform LetIn reduction now. --- helm/ocaml/cic_proof_checking/cicTypeChecker.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 28089b4cc..c86a27ad0 100644 --- 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 *) -- 2.39.2