init_cache_and_tables ~dbd flags.use_library true true false universe
(proof'''',newmeta)
in
- prerr_endline "chiamo given clause";
Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive
max_int max_int flags.timeout
with
| None, _,_,_ ->
raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle")))
| Some (_,proof''''',_), active,passive,_ ->
- prerr_endline "torno";
-
proof''''',
ProofEngineHelpers.compare_metasenvs ~oldmetasenv
~newmetasenv:(let _,m,_subst,_,_, _ = proof''''' in m), active, passive