| NCicEnvironment.ObjectNotFound s as e ->
raise (Error (lazy "eq_coerc non yet defined",Some e))
| Error _ as e -> debug_print (lazy "error"); raise e
+(* FG: for now we catch TypeCheckerFailure; to be understood *)
+ | NCicTypeChecker.TypeCheckerFailure _ ->
+ debug_print (lazy "TypeCheckerFailure");
+ raise (Error (lazy "no proof found",None))
;;
let compare_statuses ~past ~present =
maxwidth : int;
maxsize : int;
maxdepth : int;
- timeout : float;
}
type cache =
maxwidth = width;
maxsize = size;
maxdepth = depth;
- timeout = Unix.gettimeofday() +. 3000.;
do_types = false;
} in
let initial_time = Unix.gettimeofday() in
fast_eq_check_tac ~params
else auto_tac ~params ?trace_ref
;;
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-