added ~delta parameter to saturate_term and used it when saturating a coercion.

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

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index e0f8fd1c79128ad1663640690a167c931ce623cb..f680b01f1e3cd2a75bc21c2b33729c8c3d8661ff 100644 (file)
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -1334,7 +1334,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                 (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
                 CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
                 " <==> " ^
-                CicMetaSubst.ppterm_in_context ~metasenv subst t context));
+                CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ 
+                "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c
+                context));
                 debug_print (lazy ("FO_UNIF_SUBST: " ^
                 CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
                 let subst,metasenv,ugraph =