X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicMetaSubst.ml;h=53efcf96edfad1adeb23704626206dbcaaa9feab;hb=9393a9f9370014c904244358abe4ec6e11a9d158;hp=5870089beda2d9f208f318cbd22789d87a60c73f;hpb=4ab6b4054730b9ed419f0c4296f9deda9ab321b2;p=helm.git diff --git a/components/cic_unification/cicMetaSubst.ml b/components/cic_unification/cicMetaSubst.ml index 5870089be..53efcf96e 100644 --- a/components/cic_unification/cicMetaSubst.ml +++ b/components/cic_unification/cicMetaSubst.ml @@ -1,4 +1,5 @@ (* Copyright (C) 2003, HELM Team. + * * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -230,7 +231,7 @@ let apply_subst_gen ~appl_fun subst term = in C.CoFix (i, fl') in - LibrarySync.merge_coercions (um_aux term) + um_aux term ;; let apply_subst =