if Utils.debug_metas then
ignore(check_for_duplicates menv "unification_aux prima di apply_subst");
let menv = Subst.apply_subst_metasenv subst menv in
if Utils.debug_metas then
ignore(check_for_duplicates menv "unification_aux prima di apply_subst");
let menv = Subst.apply_subst_metasenv subst menv in
- let _ = check_for_duplicates menv "unif_aux after" in
- check_metasenv "unification_aux after 1" menv;
- subst, menv, ug
+ if Utils.debug_metas then
+ (let _ = check_for_duplicates menv "unif_aux after" in
+ check_metasenv "unification_aux after 1" menv);
+ subst, menv, ug