C.Lambda
(ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')
in
- let fresh_meta = ProofEngineHelpers.new_meta proof in
- let irl =
- ProofEngineHelpers.identity_relocation_list_for_metavariable context in
+ let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
+ let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
let (proof',goals) =
C.Lambda
(ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')
in
- let fresh_meta = ProofEngineHelpers.new_meta proof in
+ let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
let irl =
- ProofEngineHelpers.identity_relocation_list_for_metavariable context in
+ CicMkImplicit.identity_relocation_list_for_metavariable context in
let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
let (proof',goals) =