better indentation

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index fe45320dd6a333387f93ef7c090bbc73a8e4dec8..2d460ff007842cc40b227ee51c5673b40f5d9c7b 100644 (file)
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -1320,69 +1320,69 @@ let auto_main flags signature (pos : 'a and_pos) cache =
             | Some pos -> move_solution_up ~unfocus:true status pos cache 
 
   and attack pos cache and_item =
-     (* show pos; *) (* uncomment to show the tree *)
-     match and_item with
-       | _, S _ -> assert false (* next would close the proof or give a D *) 
-       | (_, depth, _),_ when Unix.gettimeofday () > flags.timeout ->
-           debug_print ~depth (lazy ("fail timeout"));
-           Gaveup 
-       | (s, depth, width), D (_, T as g) when not flags.do_types -> 
-           debug_print ~depth (lazy "skip goal in Type");
-           next ~unfocus:true (solved g depth width s pos) cache
-       | (_,depth,_), D _ when depth > flags.maxdepth -> 
-           debug_print ~depth (lazy "fail depth");
-           next_choice (failed pos) cache
-       | (_,depth,size), D _ when size > flags.maxsize -> 
-           debug_print ~depth (lazy "fail size");
-           next_choice (failed pos) cache
-       | (s,depth,size), D (gno,_ as g) -> 
-           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));
-              next ~unfocus:false (solved g depth size s pos) cache
-           | Some gty ->
-              let s, gty = apply_subst s (ctx_of gty) gty in
-              debug_print ~depth (lazy ("EXAMINE: "^ ppterm s gty));
-              match cache_examine cache gty with
-              | `Failed_in d when d <= depth -> 
-                 debug_print ~depth(lazy("fail depth (c): "^string_of_int gno));
-                  next_choice (failed pos) cache
-              | `UnderInspection -> 
-                  debug_print ~depth (lazy("fail loop: "^string_of_int gno));
-                  next_choice (failed pos) cache
-              | `Succeded t -> 
-                  debug_print ~depth (lazy("success (c): "^string_of_int gno));
-                  let s = put_in_subst s g t gty in
-                  next ~unfocus:true (solved g depth size s pos) cache
-              | `Notfound 
-              | `Failed_in _ -> 
-                  (* 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)
-                  else
-                  let cache = cache_add_underinspection cache gty depth in
-                  debug_print ~depth (lazy ("INSPECTING: " ^ 
-                    string_of_int gno ^ "("^ string_of_int size ^ ") "));
-                  let subgoals, cache = 
-                    do_something signature flags s gno depth gty cache
-                  in
-                  if subgoals = [] then (* this goal has failed *)
-                    next_choice (failed pos) cache
-                  else
-                    let size_gl l = List.length (prop_only l) in
-                    let subtrees = 
-                      List.map
-                        (fun (_cand,depth_incr,s,gl) ->
-                          D(gno,P), 
-                          T.Node (`And (s,depth+depth_incr,size+size_gl gl), 
-                                  List.map (fun g -> D g,T.Nil) gl))
-                        subgoals
-                    in
-                     next ~unfocus:true 
-                       (Z.inject (T.Node (`Or,subtrees)) pos) cache
+    (* show pos; *) (* uncomment to show the tree *)
+    match and_item with
+    | _, S _ -> assert false (* next would close the proof or give a D *) 
+    | (_, depth, _),_ when Unix.gettimeofday () > flags.timeout ->
+        debug_print ~depth (lazy ("fail timeout"));
+        Gaveup 
+    | (s, depth, width), D (_, T as g) when not flags.do_types -> 
+        debug_print ~depth (lazy "skip goal in Type");
+        next ~unfocus:true (solved g depth width s pos) cache
+    | (_,depth,_), D _ when depth > flags.maxdepth -> 
+        debug_print ~depth (lazy "fail depth");
+        next_choice (failed pos) cache
+    | (_,depth,size), D _ when size > flags.maxsize -> 
+        debug_print ~depth (lazy "fail size");
+        next_choice (failed pos) cache
+    | (s,depth,size), D (gno,_ as g) -> 
+        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));
+           next ~unfocus:false (solved g depth size s pos) cache
+        | Some gty ->
+           let s, gty = apply_subst s (ctx_of gty) gty in
+           debug_print ~depth (lazy ("EXAMINE: "^ ppterm s gty));
+           match cache_examine cache gty with
+           | `Failed_in d when d <= depth -> 
+               debug_print ~depth(lazy("fail depth (c): "^string_of_int gno));
+               next_choice (failed pos) cache
+           | `UnderInspection -> 
+               debug_print ~depth (lazy("fail loop: "^string_of_int gno));
+               next_choice (failed pos) cache
+           | `Succeded t -> 
+               debug_print ~depth (lazy("success (c): "^string_of_int gno));
+               let s = put_in_subst s g t gty in
+               next ~unfocus:true (solved g depth size s pos) cache
+           | `Notfound 
+           | `Failed_in _ -> 
+               (* 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)
+               else
+               let cache = cache_add_underinspection cache gty depth in
+               debug_print ~depth (lazy ("INSPECTING: " ^ 
+                 string_of_int gno ^ "("^ string_of_int size ^ ") "));
+               let subgoals, cache = 
+                 do_something signature flags s gno depth gty cache
+               in
+               if subgoals = [] then (* this goal has failed *)
+                 next_choice (failed pos) cache
+               else
+                 let size_gl l = List.length (prop_only l) in
+                 let subtrees = 
+                   List.map
+                     (fun (_cand,depth_incr,s,gl) ->
+                       D(gno,P), 
+                       T.Node (`And (s,depth+depth_incr,size+size_gl gl), 
+                               List.map (fun g -> D g,T.Nil) gl))
+                     subgoals
+                 in
+                  next ~unfocus:true 
+                    (Z.inject (T.Node (`Or,subtrees)) pos) cache
   in
     (next ~unfocus:true pos cache : 'a auto_result)
 ;;