changed stack entry representation

diff --git a/helm/ocaml/tactics/continuationals.ml b/helm/ocaml/tactics/continuationals.ml
index b720b6b7059d4a9e293f8b3e92b45ec1d01595f8..fd965dddd62a6b7886a092ba8c63431c3d89819c 100644 (file)
--- a/helm/ocaml/tactics/continuationals.ml
+++ b/helm/ocaml/tactics/continuationals.ml
@@ -37,11 +37,11 @@ module Stack =
 struct
   type switch = Open of goal | Closed of goal
   type locator = int * switch
-  type tag = BranchTag | FocusTag | NoTag
+  type tag = [ `BranchTag | `FocusTag | `NoTag ]
   type entry = locator list * locator list * locator list * tag
   type t = entry list
 
-  let empty = [ [], [], [], NoTag ]
+  let empty = [ [], [], [], `NoTag ]
 
   let fold ~env ~cont ~todo init stack =
     let rec aux acc depth =
@@ -108,12 +108,12 @@ struct
   let is_empty =
     function
     | [] -> assert false
-    | [ [], [], [], NoTag ] -> true
+    | [ [], [], [], `NoTag ] -> true
     | _ -> false
 
   let of_metasenv metasenv =
     let goals = List.map (fun (g, _, _) -> g) metasenv in
-    [ zero_pos goals, [], [], NoTag ]
+    [ zero_pos goals, [], [], `NoTag ]
 
   let head_switches =
     function
@@ -159,7 +159,7 @@ struct
     in
     let pp_loc (i, s) = string_of_int i ^ pp_switch s in
     let pp_env env = sprintf "[%s]" (String.concat ";" (List.map pp_loc env)) in
-    let pp_tag = function BranchTag -> "B" | FocusTag -> "F" | NoTag -> "N" in
+    let pp_tag = function `BranchTag -> "B" | `FocusTag -> "F" | `NoTag -> "N" in
     let pp_stack_entry (env, todo, cont, tag) =
       sprintf "(%s, %s, %s, %s)" (pp_env env) (pp_env todo) (pp_env cont)
         (pp_tag tag)
@@ -310,28 +310,28 @@ struct
           | [] | [ _ ] -> fail (lazy "too few goals to branch");
           | loc :: loc_tl ->
               new_stack
-                (([ loc ], [], [], BranchTag) :: (loc_tl, t, k, tag) :: s))
-      | Shift, (g, t, k, BranchTag) :: (g', t', k', tag) :: s ->
+                (([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s))
+      | Shift, (g, t, k, `BranchTag) :: (g', t', k', tag) :: s ->
           (match g' with
           | [] -> fail (lazy "no more goals to shift")
           | loc :: loc_tl ->
               new_stack
-                (([ loc ], t @+ filter_open g, [], BranchTag)
+                (([ loc ], t @+ filter_open g, [],`BranchTag)
                 :: (loc_tl, t', k', tag) :: s))
       | Shift, _ -> fail (lazy "can't shift goals here")
-      | Pos i, ([ loc ], [], [], BranchTag) :: (g', t', k', tag) :: s
+      | Pos i, ([ loc ], [], [],`BranchTag) :: (g', t', k', tag) :: s
         when is_fresh loc ->
           let loc_i, g' = extract_pos i g' in
           new_stack
-            (([ loc_i ], [], [], BranchTag)
+            (([ loc_i ], [], [],`BranchTag)
              :: ([ loc ] @+ g', t', k', tag) :: s)
-      | Pos i, (g, t, k, BranchTag) :: (g', t', k', tag) :: s ->
+      | Pos i, (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
           let loc_i, g' = extract_pos i g' in
           new_stack
-            (([ loc_i ], [], [], BranchTag)
+            (([ loc_i ], [], [],`BranchTag)
              :: (g', t' @+ filter_open g, k', tag) :: s)
       | Pos _, _ -> fail (lazy "can't use relative positioning here")
-      | Merge, (g, t, k, BranchTag) :: (g', t', k', tag) :: s ->
+      | Merge, (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
           new_stack ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s)
       | Merge, _ -> fail (lazy "can't merge goals here")
       | Focus [], _ -> assert false
@@ -345,8 +345,8 @@ struct
               if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then
                 fail (lazy (sprintf "goal %d not found (or closed)" g)))
             gs;
-          new_stack ((zero_pos gs, [], [], FocusTag) :: deep_close gs s)
-      | Unfocus, ([], [], [], FocusTag) :: s -> new_stack s
+          new_stack ((zero_pos gs, [], [], `FocusTag) :: deep_close gs s)
+      | Unfocus, ([], [], [], `FocusTag) :: s -> new_stack s
       | Unfocus, _ -> fail (lazy "can't unfocus, some goals are still open")
     in
     debug_print (lazy (sprintf "EVAL CONT %s -> %s" (pp_t cmd) (pp stack)));

diff --git a/helm/ocaml/tactics/continuationals.mli b/helm/ocaml/tactics/continuationals.mli
index 176fd58b245e6473a7f3ef8dbdea82785df6fcf9..d40202d4b37e2a92f1ba878a0581fdbf50501bcb 100644 (file)
--- a/helm/ocaml/tactics/continuationals.mli
+++ b/helm/ocaml/tactics/continuationals.mli
@@ -33,7 +33,7 @@ module Stack:
 sig
   type switch = Open of goal | Closed of goal
   type locator = int * switch
-  type tag = BranchTag | FocusTag | NoTag
+  type tag = [ `BranchTag | `FocusTag | `NoTag ]
   type entry = locator list * locator list * locator list * tag
   type t = entry list
 

diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml
index 8281c9452e7035bd958f579bef38474810e21302..b0a9f452eda2fef9b064517aa663a8c1b40eb3ae 100644 (file)
--- a/helm/ocaml/tactics/tacticals.ml
+++ b/helm/ocaml/tactics/tacticals.ml
@@ -315,7 +315,7 @@ struct
   let mk_tactic f =
     ProofEngineTypes.mk_tactic
       (fun (proof, goal) as pstatus ->
-        let stack = [ [ 1, Stack.Open goal ], [], [], Stack.NoTag ] in
+        let stack = [ [ 1, Stack.Open goal ], [], [], `NoTag ] in
         let istatus = pstatus, stack in
 (*         let ostatus = f istatus in
         let ((proof, opened, _), _) = ostatus in *)