New tactic: inversion.

[helm.git] / helm / matita / matitaMathView.ml

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index a7299879a3a3292ab31785e0e7a558a74a4599c1..93adb1c90fc529356bb4db6457aaf96fa1d24357 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -245,12 +245,12 @@ object (self)
       let pat = self#tactic_text_pattern_of_selection in
       let statement =
         let loc = DisambiguateTypes.dummy_floc in
+        "\n" ^
         GrafiteAstPp.pp_executable ~term_pp:(fun s -> s)
           ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
           (GrafiteAst.Tactical (loc,
             GrafiteAst.Tactic (loc, GrafiteAst.Reduce (loc, kind, pat)),
             Some (GrafiteAst.Semicolon loc))) in
-      HLog.debug ("soon I'll evaluate: " ^ statement);
       (MatitaScript.current ())#advance ~statement () in
     connect_menu_item copy gui#copy;
     connect_menu_item normalize (reduction_action `Normalize);