| Some _ ->
let _, metasenv, _, _ = proof in
let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in
- full || (Inference.term_is_equality meta_goal)
+ full || (Equality.term_is_equality meta_goal)
in
if paramodulation_ok then (
debug_print (lazy "USO PARAMODULATION...");
(* try *)
- Saturation.saturate dbd ~depth ~width ~full (proof, goal)
+ try
+ Saturation.saturate dbd ~depth ~width ~full (proof, goal)
+ with exn ->
+ prerr_endline (Saturation.get_stats ());
+ raise exn
+
(* with ProofEngineTypes.Fail _ -> *)
(* normal_auto () *)
) else