| (D (_,_,T))::tl -> aux tl
| _ -> false
and no_progress variant = function
- | [] -> prerr_endline "++++++++++++++++++++++++ no_progress"; true
+ | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true
| D ((n,_,P) as g)::tl ->
(match calculate_goal_ty g subst menv with
| None -> no_progress variant tl
(debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int gsize));
aux tables maxm flags cache orlist)
else if prunable_for_size flags s m todo then
- (prerr_endline ("POTO at depth: "^(string_of_int depth));
+ (debug_print (lazy ("POTO at depth: "^(string_of_int depth)));
aux tables maxm flags cache orlist)
else
(* still to be proved *)
in
match auto_main tables newmeta context flags universe cache [elem] with
| Proved (metasenv,subst,_, tables,cache,_) ->
- prerr_endline
- ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
+ (*prerr_endline
+ ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));*)
let proof,metasenv =
ProofEngineHelpers.subst_meta_and_metasenv_in_proof
proof goal subst metasenv
(* we take the whole universe (no signature filtering) *)
init_cache_and_tables false true false true universe (proof,goal)
in
- let initgoal = [], [], ty in
+ let initgoal = [], metasenv, ty in
let table =
let equalities = (Saturation.list_of_passive passive) in
(* we demodulate using both actives passives *)
let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
- let initgoal = [], [], ty in
+ let initgoal = [], metasenv, ty in
let eq_uri = eq_of_goal ty in
let (active,passive,bag), cache, maxm =
init_cache_and_tables