X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_proof_checking%2FcicReduction.ml;h=63a8f550323a8ac9ad9fd8fd90b609158ef230f4;hb=acf29bdbdcdc6ad8c2d9d27e8a47500981b605cd;hp=55ffb8edb99787b69b77fa2218caf8f96b0b21dd;hpb=5530db2f72548a8c579ae5f9868cbd38290eb065;p=helm.git

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