- 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