1. The last commit that fixed unification of compound coercions with

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

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index afd74d75672ddf5b31ee53735ea56bc74694de0e..5870089beda2d9f208f318cbd22789d87a60c73f 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -230,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 =