]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_unification/cicMetaSubst.ml
removed no longer used METAs
[helm.git] / helm / ocaml / cic_unification / cicMetaSubst.ml
index 718951c68a579756e4c4bd1d0994c835d28e2bac..5870089beda2d9f208f318cbd22789d87a60c73f 100644 (file)
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
 open Printf
 
 (* PROFILING *)
@@ -228,7 +230,7 @@ let apply_subst_gen ~appl_fun subst term =
        in
        C.CoFix (i, fl')
  in
- um_aux term
+  LibrarySync.merge_coercions (um_aux term)
 ;;
 
 let apply_subst =