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
*)
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