From 4f00a766afd24d51314badcab74cea2ccf623e28 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 4 Nov 2005 09:06:29 +0000
Subject: [PATCH] changed stack entry representation

---
 helm/ocaml/tactics/continuationals.ml  | 30 +++++++++++++-------------
 helm/ocaml/tactics/continuationals.mli |  2 +-
 helm/ocaml/tactics/tacticals.ml        |  2 +-
 3 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/helm/ocaml/tactics/continuationals.ml b/helm/ocaml/tactics/continuationals.ml
index b720b6b70..fd965dddd 100644
--- 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 176fd58b2..d40202d4b 100644
--- 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 8281c9452..b0a9f452e 100644
--- 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 *)
-- 
2.39.2