From: Enrico Tassi Date: Wed, 1 Jun 2005 11:01:10 +0000 (+0000) Subject: added C.Appl [] case X-Git-Tag: PRE_INDEX_1~83 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eab8828b82bf59763dd985b1abd211fee5e6a095;p=helm.git added C.Appl [] case --- diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml index 55ffb8edb..63a8f5503 100644 --- a/helm/ocaml/cic_proof_checking/cicReduction.ml +++ b/helm/ocaml/cic_proof_checking/cicReduction.ml @@ -1066,6 +1066,7 @@ let rec normalize ?(delta=true) ?(subst=[]) ctx term = let s' = aux ctx s in C.LetIn (n, s, aux ((def n s')::ctx) t) | C.Appl (h::l) -> C.Appl (h::(List.map (aux ctx) l)) + | C.Appl [] -> assert false | C.Const (uri,exp_named_subst) -> C.Const (uri, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst) | C.MutInd (uri,typeno,exp_named_subst) -> @@ -1079,9 +1080,9 @@ let rec normalize ?(delta=true) ?(subst=[]) ctx term = | C.CoFix _ -> t let normalize ?delta ?subst ctx term = - prerr_endline ("NORMALIZE:" ^ CicPp.ppterm term); +(* prerr_endline ("NORMALIZE:" ^ CicPp.ppterm term); *) let t = normalize ?delta ?subst ctx term in - prerr_endline ("NORMALIZED:" ^ CicPp.ppterm t); +(* prerr_endline ("NORMALIZED:" ^ CicPp.ppterm t); *) t