From: Claudio Sacerdoti Coen Date: Fri, 8 Jul 2005 08:10:45 +0000 (+0000) Subject: An impossible case changed to an assert false. X-Git-Tag: V_0_7_1~4 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e1518f70bdddd0bc19cdf34e6fc9564e158ae35e;p=helm.git An impossible case changed to an assert false. --- diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml index 8b9a0d22e..aaca61942 100644 --- a/helm/ocaml/cic_proof_checking/cicReduction.ml +++ b/helm/ocaml/cic_proof_checking/cicReduction.ml @@ -1063,8 +1063,8 @@ let rec normalize ?(delta=true) ?(subst=[]) ctx term = let s' = aux ctx s in C.Lambda (n, s', aux ((decl n s')::ctx) t) | C.LetIn (n,s,t) -> - let s' = aux ctx s in - C.LetIn (n, s, aux ((def n s')::ctx) t) + (* the term is already in weak head normal form *) + assert false | C.Appl (h::l) -> C.Appl (h::(List.map (aux ctx) l)) | C.Appl [] -> assert false | C.Const (uri,exp_named_subst) -> @@ -1076,6 +1076,7 @@ let rec normalize ?(delta=true) ?(subst=[]) ctx term = List.map (fun (n,t) -> n,aux ctx t) exp_named_subst) | C.MutCase (sp,i,outt,t,pl) -> C.MutCase (sp,i, aux ctx outt, aux ctx t, List.map (aux ctx) pl) +(*CSC: to be completed, I suppose *) | C.Fix _ -> t | C.CoFix _ -> t