From eab8828b82bf59763dd985b1abd211fee5e6a095 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 1 Jun 2005 11:01:10 +0000 Subject: [PATCH] added C.Appl [] case --- helm/ocaml/cic_proof_checking/cicReduction.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) 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 -- 2.39.2