better comments and indentation

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index 267f3b10bb1dc30c6fd604f9c86be623a5c13417..fe45320dd6a333387f93ef7c090bbc73a8e4dec8 100644 (file)
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -1320,7 +1320,7 @@ 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; *)
+     (* 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 ->
@@ -1336,8 +1336,7 @@ let auto_main flags signature (pos : 'a and_pos) cache =
            debug_print ~depth (lazy "fail size");
            next_choice (failed pos) cache
        | (s,depth,size), D (gno,_ as g) -> 
-           (* assert unexplored *)
-           assert (Z.eject pos = ZipTree.Nil);
+           assert (Z.eject pos = T.Nil); (*subtree must be unexplored *)
            match calculate_goal_ty g s with
            | None -> 
               debug_print 
@@ -1359,7 +1358,7 @@ let auto_main flags signature (pos : 'a and_pos) cache =
                   next ~unfocus:true (solved g depth size s pos) cache
               | `Notfound 
               | `Failed_in _ -> 
-                 (* more depth or is the first time we see the goal *)
+                  (* 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)
@@ -1367,7 +1366,6 @@ let auto_main flags signature (pos : 'a and_pos) cache =
                   let cache = cache_add_underinspection cache gty depth in
                   debug_print ~depth (lazy ("INSPECTING: " ^ 
                     string_of_int gno ^ "("^ string_of_int size ^ ") "));
-                  (* pos are possible computations for proving gty *)
                   let subgoals, cache = 
                     do_something signature flags s gno depth gty cache
                   in
@@ -1376,15 +1374,15 @@ let auto_main flags signature (pos : 'a and_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), 
-                        ZipTree.Node (
-                          `And (s,depth+depth_incr,size+size_gl gl), 
-                          List.map (fun g -> D g,ZipTree.Nil) gl))
+                      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 (ZipTree.Node (`Or,subtrees)) pos) cache
+                       (Z.inject (T.Node (`Or,subtrees)) pos) cache
   in
     (next ~unfocus:true pos cache : 'a auto_result)
 ;;
@@ -1411,8 +1409,8 @@ let auto_tac ~params:(_univ,flags) status =
   let size  = int "size" flags 10 in 
   let width = int "width" flags (3+List.length goals) in 
   (* XXX fix sort *)
-  let goals = List.map (fun i -> D(i,P), ZipTree.Nil) goals in
-  let elems = Z.start (ZipTree.Node (`And(status,0,0),goals)) in
+  let goals = List.map (fun i -> D(i,P), T.Nil) goals in
+  let elems = Z.start (T.Node (`And(status,0,0),goals)) in
   let signature = () in
   let flags = { 
           maxwidth = width;