*)
let new_meta_of_proof ~proof:(_, metasenv, _, _) =
- CicMkImplicit.new_meta metasenv
+ CicMkImplicit.new_meta metasenv []
let subst_meta_in_proof proof meta term newmetasenv =
let uri,metasenv,bo,ty = proof in
- let subst_in = CicMetaSubst.apply_subst [meta,term] in
+ (* empty context is ok for term since it wont be used by apply_subst *)
+ let subst_in = CicMetaSubst.apply_subst [meta,([], term)] in
let metasenv' =
newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
in