+let relocate newmeta menv =
+ let subst, metasenv, newmeta =
+ List.fold_right
+ (fun (i, context, ty) (subst, menv, maxmeta) ->
+ let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in
+ let newsubst = (i, (context, (Cic.Meta (maxmeta, irl)), ty)) in
+ let newmeta = maxmeta, context, ty in
+ newsubst::subst, newmeta::menv, maxmeta+1)
+ menv ([], [], newmeta+1)
+ in
+ let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
+ let subst =
+ List.map
+ (fun (i, (context, term, ty)) ->
+ let context = CicMetaSubst.apply_subst_context subst context in
+ let term = CicMetaSubst.apply_subst subst term in
+ let ty = CicMetaSubst.apply_subst subst ty in
+ (i, (context, term, ty))) subst in
+ subst, metasenv, newmeta
+
+
+let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) =
+ (* debug
+ let _ , eq =
+ fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
+ prerr_endline (string_of_equality eq); *)
+ let subst, metasenv, newmeta = relocate newmeta menv in
+ let ty = CicMetaSubst.apply_subst subst ty in
+ let left = CicMetaSubst.apply_subst subst left in
+ let right = CicMetaSubst.apply_subst subst right in
+ let args = List.map (CicMetaSubst.apply_subst subst) args in
+ let rec fix_proof = function
+ | NoProof -> NoProof
+ | BasicProof term -> BasicProof (CicMetaSubst.apply_subst subst term)
+ | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) ->
+ ProofBlock (subst' @ subst, eq_URI, namety, bo, (pos, eq), p)
+ | p -> assert false
+ in
+ let metas = (metas_of_term left)@(metas_of_term right)@(metas_of_term ty) in
+ let metasenv = List.filter (fun (i, _, _) -> List.mem i metas) metasenv in
+ let eq = (w, fix_proof p, (ty, left, right, o), metasenv, args) in
+ (* debug prerr_endline (string_of_equality eq); *)
+ newmeta, eq
+