repl proof
in
let newcicp,np,subst,cicmenv =
- cicproof,np, subst, (m @ menv)
+ cicproof,np, subst, Equality.apply_subst_metasenv subst (m @ menv)
in
Some
((newcicp,np,subst,cicmenv),
let cic_proof = Equality.build_proof_term_old proof in
(* generation of the new proof *)
- let cic_proof_new,cic_proof_new_menv =
+ let cic_proof_new =
Equality.build_goal_proof
goalproof (Equality.build_proof_term_new newproof)
in
- let newproof_menv =
- Equality.apply_subst_metasenv subsumption_subst
- (newproof_menv @ cic_proof_new_menv)
- in
let cic_proof_new =
Equality.apply_subst subsumption_subst cic_proof_new
in