X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=fbde6a82093c17f316e14cbc6cd32da06d7219c0;hb=46f19eadce5f3a11c0ae26934fd8d1b597906416;hp=621834e3326dd4fbc124dfbec1138433ed9e42e2;hpb=0575a1cb077087970f311b48f2e45dc4a01a6867;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 621834e33..fbde6a820 100644
--- 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