;;
*)
+(*
let paramodulation_tactic = ref
(fun dbd ?full ?depth ?width status ->
raise (ProofEngineTypes.Fail (lazy "Not Ready yet...")));;
let term_is_equality = ref
(fun term -> debug_print (lazy "term_is_equality E` DUMMY!!!!"); false);;
-
+*)
let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation
?full ~(dbd:HMysql.dbd) () =
| Some _ ->
let _, metasenv, _, _ = proof in
let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in
- full || (!term_is_equality meta_goal)
+ full || (Inference.term_is_equality meta_goal)
in
if paramodulation_ok then (
debug_print (lazy "USO PARAMODULATION...");
(* try *)
- !paramodulation_tactic dbd ~depth ~width ~full (proof, goal)
+ Saturation.saturate dbd ~depth ~width ~full (proof, goal)
(* with ProofEngineTypes.Fail _ -> *)
(* normal_auto () *)
) else