removed debug prerr_endline

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 621834e3326dd4fbc124dfbec1138433ed9e42e2..fbde6a82093c17f316e14cbc6cd32da06d7219c0 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -29,7 +29,7 @@ exception RefineFailure of string;;
 exception Uncertain of string;;
 exception AssertFailure of string;;
 
-let debug_print = prerr_endline
+let debug_print = fun _ -> ()
 
 let fo_unif_subst subst context metasenv t1 t2 ugraph =
   try
@@ -47,19 +47,22 @@ let rec split l n =
 ;;
 
 let look_for_coercion src tgt =
+  None
+  (*
   if (src = (CicUtil.term_of_uri "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)")) &&
      (tgt = (CicUtil.term_of_uri "cic:/Coq/Reals/Rdefinitions/R.con")) 
   then
     begin
-    prerr_endline "TROVATA coercion";
+    debug_print "TROVATA coercion";
     Some (CicUtil.term_of_uri "cic:/Coq/Reals/Raxioms/INR.con")
     end
   else 
     begin
-    prerr_endline (sprintf "NON TROVATA la coercion %s %s" (CicPp.ppterm src) 
+    debug_print (sprintf "NON TROVATA la coercion %s %s" (CicPp.ppterm src) 
       (CicPp.ppterm tgt));
     None
     end
+  *)
 ;;
 
 
@@ -784,7 +787,7 @@ and type_of_aux' metasenv context t ugraph =
       try
        fo_unif_subst subst context metasenv hetype hetype' ugraph
       with exn ->
-       prerr_endline (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
+       debug_print (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
                         (CicPp.ppterm hetype)
                         (CicPp.ppterm hetype')
                         (CicMetaSubst.ppmetasenv metasenv [])
@@ -877,6 +880,13 @@ and type_of_aux' metasenv context t ugraph =
     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) 
 ;;
 
+let type_of_aux' metasenv context term ugraph =
+  try 
+    type_of_aux' metasenv context term ugraph
+  with 
+    CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)
+    
+
 (* DEBUGGING ONLY 
 let type_of_aux' metasenv context term =
  try