better indentation

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index 2d460ff007842cc40b227ee51c5673b40f5d9c7b..b2620735d08a6d3112d7a37d28dbec05628d4ea6 100644 (file)
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -1339,8 +1339,7 @@ let auto_main flags signature (pos : 'a and_pos) cache =
         assert (Z.eject pos = T.Nil); (*subtree must be unexplored *)
         match calculate_goal_ty g s with
         | None -> 
-           debug_print 
-             ~depth (lazy ("success side effect: " ^ string_of_int gno));
+           debug_print ~depth (lazy("success side effect: "^string_of_int gno));
            next ~unfocus:false (solved g depth size s pos) cache
         | Some gty ->
            let s, gty = apply_subst s (ctx_of gty) gty in
@@ -1361,7 +1360,7 @@ let auto_main flags signature (pos : 'a and_pos) cache =
                (* more depth than before or first time we see the goal *)
                if prunable s gty () then
                  (debug_print ~depth (lazy( "fail one father is equal"));
-                 next_choice (failed pos) cache)
+                  next_choice (failed pos) cache)
                else
                let cache = cache_add_underinspection cache gty depth in
                debug_print ~depth (lazy ("INSPECTING: " ^