removed debug prerr_endline

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

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 25db7d9154b5a6e785a6d90cc4e20159bf631533..3545f6c0e22bf9b3c6223ceb820fc3c4bd9af5c2 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -29,7 +29,7 @@ exception UnificationFailure of string;;
 exception Uncertain of string;;
 exception AssertFailure of string;;
 
-let debug_print = prerr_endline
+let debug_print = fun _ -> () 
 
 let type_of_aux' metasenv subst context term ugraph =
   try 
@@ -305,7 +305,7 @@ and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
                            with
                                Uncertain _
                              | UnificationFailure _ ->
-prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)); 
+debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)); 
                                  let metasenv, subst = 
                                    CicMetaSubst.restrict 
                                      subst [(n,j)] metasenv in
@@ -359,9 +359,9 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str
             with 
                UnificationFailure msg 
              | Uncertain msg ->
-                 prerr_endline msg;raise (UnificationFailure msg) 
+                 (* debug_print msg; *)raise (UnificationFailure msg) 
               | AssertFailure _ ->
-                 prerr_endline "siamo allo huge hack";
+                 debug_print "siamo allo huge hack";
                  (* TODO huge hack!!!!
                   * we keep on unifying/refining in the hope that 
                   * the problem will be eventually solved. 
@@ -607,12 +607,12 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str
            C.Prod _ -> 
              fo_unif_subst test_equality_only 
                subst context metasenv t1' t2 ugraph     
-         | _ -> (* raise (UnificationFailure "9")) *)
-              raise 
+         | _ -> raise (UnificationFailure "9"))
+     (*         raise 
                (UnificationFailure (sprintf
                   "Can't unify %s with %s because they are not convertible"
                   (CicMetaSubst.ppterm subst t1) 
-                  (CicMetaSubst.ppterm subst t2))))
+                  (CicMetaSubst.ppterm subst t2))))*)
    | (_,_) ->
        let b,ugraph1 = 
         R.are_convertible ~subst ~metasenv context t1 t2 ugraph