Much ado about nothing:

[helm.git] / matita / matitaMathView.ml

diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml
index 4252014bd83115bfae8ad9927dfd88cabcef0967..3b4c566e2a9a42c50c80bf7011cf37eabe0831a2 100644 (file)
--- a/matita/matitaMathView.ml
+++ b/matita/matitaMathView.ml
@@ -303,9 +303,9 @@ object (self)
         "\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
+          (GrafiteAst.Tactic (loc,
+            Some (GrafiteAst.Reduce (loc, kind, pat)),
+            GrafiteAst.Semicolon loc)) in
       (MatitaScript.current ())#advance ~statement () in
     connect_menu_item copy gui#copy;
     connect_menu_item normalize (reduction_action `Normalize);