added support for "polymorphic" coercions

[helm.git] / components / cic_unification / cicMetaSubst.ml

diff --git a/components/cic_unification/cicMetaSubst.ml b/components/cic_unification/cicMetaSubst.ml
index 5870089beda2d9f208f318cbd22789d87a60c73f..53efcf96edfad1adeb23704626206dbcaaa9feab 100644 (file)
--- 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 =