From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 28 Oct 2009 13:38:21 +0000 (+0000)
Subject: better indentation
X-Git-Tag: make_still_working~3242
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cd415135f0bcf53f10ed7649fcacc3247bc7a3f1;p=helm.git

better indentation
---

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index 2d460ff00..b2620735d 100644
--- 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: " ^