- let proof = uri, other_menv@metasenv, subst, meta_proof, term_to_prove, attrs in
+ let newmetasenv =
+ other_menv @
+ List.filter
+ (fun x,_,_ -> not (List.exists (fun y,_,_ -> x=y) other_menv)) metasenv
+ in
+ let proof = uri, newmetasenv, subst, meta_proof, term_to_prove, attrs in