X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=0e119f34b73949079b03cce21be67e0173f8d6ef;hb=a338e0effc313d4da419d6df91397232c24170d9;hp=d5cf3892270f3c05c81c9d4decb82e268c0b65cf;hpb=0e3324ad8e6a552ee89f02371412f7bc2e83379f;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index d5cf38922..0e119f34b 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -226,9 +226,7 @@ and instantiate test_eq_only metasenv subst context n lc t swap =
   in
          pp (lazy(string_of_int n ^ " := 222 = "^
            NCicPp.ppterm ~metasenv ~subst ~context:ctx t
-         ^ "\n" ^ NCicPp.ppmetasenv ~subst metasenv
-         
-         ));
+         ^ "\n" ^ NCicPp.ppmetasenv ~subst metasenv));
   (* Unifying the types may have already instantiated n. *)
   try
     let _, _,oldt,_ = NCicUtils.lookup_subst n subst in