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
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
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.
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