From f268a4b949ad0ac525f73dbd5116722c2ca6f552 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 20 Jul 2005 16:25:32 +0000 Subject: [PATCH] Debugging code commented out. --- helm/ocaml/cic_proof_checking/cicElim.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml index 869d5d08b..e3fca907d 100644 --- a/helm/ocaml/cic_proof_checking/cicElim.ml +++ b/helm/ocaml/cic_proof_checking/cicElim.ml @@ -28,9 +28,8 @@ open Printf exception Elim_failure of string exception Can_t_eliminate -(* -let debug_print = fun _ -> () *) -let debug_print = prerr_endline +let debug_print = fun _ -> () +(*let debug_print = prerr_endline *) let counter = ref ~-1 ;; @@ -367,14 +366,18 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno = in add_params (fun b s t -> Cic.Lambda (b, s, t)) leftno ty cic in +(* debug_print (CicPp.ppterm eliminator_type); debug_print (CicPp.ppterm eliminator_body); +*) let eliminator_type = FreshNamesGenerator.mk_fresh_names [] [] [] eliminator_type in let eliminator_body = FreshNamesGenerator.mk_fresh_names [] [] [] eliminator_body in +(* debug_print (CicPp.ppterm eliminator_type); debug_print (CicPp.ppterm eliminator_body); +*) let (computed_type, ugraph) = try CicTypeChecker.type_of_aux' [] [] eliminator_body CicUniv.empty_ugraph -- 2.39.2