~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
in
C.Lambda
- (ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')
+ (FreshNamesGenerator.mk_fresh_name context C.Anonymous ty, ty, gty'')
in
let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
in
C.Lambda
- (ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')
+ (FreshNamesGenerator.mk_fresh_name context C.Anonymous ty, ty, gty'')
in
let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
let irl =