From eab8828b82bf59763dd985b1abd211fee5e6a095 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
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