X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcicCoercion.ml;h=f06035604535dcd5a132f2667292f6318dc15fd2;hb=cee1c02ad6a113b711b9d93176296cf16b9ec351;hp=33309f109e6c48d2b9f11b5885170ac4d65bab8c;hpb=abd2098b6c4a40b36bb4b950c607eb4b4a7852bc;p=helm.git

diff --git a/helm/software/components/library/cicCoercion.ml b/helm/software/components/library/cicCoercion.ml
index 33309f109..f06035604 100644
--- a/helm/software/components/library/cicCoercion.ml
+++ b/helm/software/components/library/cicCoercion.ml
@@ -216,7 +216,7 @@ let generate_composite_closure rt c1 c2 univ arity =
         let body_metasenv = order_body_menv term body_metasenv in
         debug_print(lazy("ORDERED_B_MENV: "^rt.RT.ppmetasenv [] body_metasenv));
         let subst = create_subst_from_metas_to_rels spline_len body_metasenv in
-        debug_print (lazy("SUBST: "^rt.RT.ppsubst subst));
+        debug_print (lazy("SUBST: "^rt.RT.ppsubst body_metasenv subst));
         let term = rt.RT.apply_subst subst term in
         debug_print (lazy ("COMPOSED SUBSTITUTED: " ^ CicPp.ppterm term));
         (match rt.RT.type_of_aux' metasenv [] term ugraph with