]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_refiner/nCicUnification.ml
removed empty lines
[helm.git] / helm / software / components / ng_refiner / nCicUnification.ml
index d5cf3892270f3c05c81c9d4decb82e268c0b65cf..0e119f34b73949079b03cce21be67e0173f8d6ef 100644 (file)
@@ -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