+ (* this is the ugly hack to debug paramod *)
+ Saturation.superposition_tac
+ ~target ~table ~subterms_only ~demod_table (proof,goal)
+ | false ->
+ (* this is the real auto *)
+ let _, metasenv, _, _ = proof in
+ let _, context, goalty = CicUtil.lookup_meta goal metasenv in
+ let use_paramodulation =
+ paramodulation && Equality.term_is_equality goalty
+ in
+ if use_paramodulation then
+ try
+ let rc =
+ Saturation.saturate
+ ~auto:(callback_for_paramodulation dbd)
+ caso_strano dbd ~depth ~width ~full
+ ?timeout (proof, goal)
+ in
+ prerr_endline (Saturation.get_stats ());rc
+ with exn ->
+ prerr_endline (Saturation.get_stats ());raise exn
+ else
+ let universe =
+ AutoTypes.universe_of_goals dbd proof [goal] AutoTypes.empty_universe
+ in
+ let universe = (* we should get back a menv too XXX *)
+ AutoTypes.universe_of_context context metasenv universe
+ in
+ let oldmetasenv = metasenv in
+ match
+ Auto.auto universe AutoTypes.cache_empty context metasenv [goal]
+ {AutoTypes.default_flags with
+ AutoTypes.maxdepth = depth;
+ AutoTypes.maxwidth = width;
+(* AutoTypes.timeout = 0; *)
+ }
+ with
+ | None,cache ->
+ raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
+ | Some (subst,metasenv),cache ->
+ let proof,metasenv =
+ ProofEngineHelpers.subst_meta_and_metasenv_in_proof
+ proof goal (CicMetaSubst.apply_subst subst) metasenv
+ in
+ let opened =
+ ProofEngineHelpers.compare_metasenvs ~oldmetasenv
+ ~newmetasenv:metasenv
+ in
+ proof,opened