if proof_menv = [] then prerr_endline "+++++++++++++++VUOTA"
else prerr_endline (CicMetaSubst.ppmetasenv [] proof_menv);
let proof, goalno = status in
- let uri, metasenv, meta_proof, term_to_prove, attrs = proof in
+ let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
let eq_uri = eq_of_goal type_of_goal in
let names = Utils.names_of_context context in
(ProofEngineHelpers.compare_metasenvs
~newmetasenv:metasenv ~oldmetasenv:proof_menv) in
let goal_proof, side_effects_t =
- let initial = (* Equality.add_subst subsumption_subst*) newproof in
+ let initial = Equality.add_subst subsumption_subst newproof in
Equality.build_goal_proof bag
eq_uri goalproof initial type_of_goal side_effects
context proof_menv
in
+(* Equality.draw_proof bag names goalproof newproof subsumption_id; *)
let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
let real_menv = fix_metasenv (proof_menv@metasenv) in
let real_menv,goal_proof =
*)
let proof, real_metasenv =
ProofEngineHelpers.subst_meta_and_metasenv_in_proof
- proof goalno (CicMetaSubst.apply_subst final_subst)
+ proof goalno final_subst
(List.filter (fun i,_,_ -> i<>goalno ) real_menv)
in
let open_goals =
let all_subsumed bag maxm status active passive =
maxmeta := maxm;
let proof, goalno = status in
- let uri, metasenv, meta_proof, term_to_prove, attrs = proof in
+ let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
let env = metasenv,context,CicUniv.empty_ugraph in
let cleaned_goal = Utils.remove_local_context type_of_goal in
let mp = max_l passive_l in
*)
let proof, goalno = status in
- let uri, metasenv, meta_proof, term_to_prove, attrs = proof in
+ let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
let eq_uri = eq_of_goal type_of_goal in
let cleaned_goal = Utils.remove_local_context type_of_goal in