X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicRefine.ml;h=f680b01f1e3cd2a75bc21c2b33729c8c3d8661ff;hb=e68d06002f901a6252bc0b6ad6b655c9acb72b0f;hp=e0f8fd1c79128ad1663640690a167c931ce623cb;hpb=1d6910f6ee5dfd0e53fcec8c020311baba922a4c;p=helm.git

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index e0f8fd1c7..f680b01f1 100644
--- 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 =