The pretty printers in CicPp now have an optional ~metasenv argument to

[helm.git] / helm / software / components / library / cicCoercion.ml

diff --git a/helm/software/components/library/cicCoercion.ml b/helm/software/components/library/cicCoercion.ml
index 33309f109e6c48d2b9f11b5885170ac4d65bab8c..f06035604535dcd5a132f2667292f6318dc15fd2 100644 (file)
--- 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