New implementation of the tactic monad.

The new implementation is made of two layers: a iolist, which is essentially
a stream without memoization, and above this a state monad. The previous
design of the extracted monad kept three distinct but similar monad
transformers: a stateT, a writerT and a readerT. We take advantage of this
similarity to pack those three transformers into only one state monad.
This makes the code cleaner and hopefully more efficient.

1 files changed, 127 insertions, 560 deletions

diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml
index cb195c5e8a..04c3c267d3 100644
--- a/proofs/proofview_gen.ml
+++ b/proofs/proofview_gen.ml
@@ -1,79 +1,44 @@
-(* This file has been generated by extraction of bootstrap/Monads.v. It
-   shouldn't be modified directly. To regenerate it run coqtop -batch
-   -impredicative-set -l bootstrap/Monads.v in Coq's source directory. *)
-
-type __ = Obj.t
-let __ = let rec f _ = Obj.repr f in Obj.repr f
-
 type ('a, 'b) list_view =
 | Nil of exn
 | Cons of 'a * 'b
 
-module IOBase = 
- struct 
-  type 'a coq_T = unit -> 'a
-  
+module IO =
+ struct
+  type 'a t = unit -> 'a
+
   type 'a coq_Ref = 'a Pervasives.ref
-  
-  (** val ret : 'a1 -> 'a1 coq_T **)
-  
+
   let ret = fun a -> (); fun () -> a
-  
-  (** val bind : 'a1 coq_T -> ('a1 -> 'a2 coq_T) -> 'a2 coq_T **)
-  
+
   let bind = fun a k -> (); fun () -> k (a ()) ()
-  
-  (** val ignore : 'a1 coq_T -> unit coq_T **)
-  
+
   let ignore = fun a -> (); fun () -> ignore (a ())
-  
-  (** val seq : unit coq_T -> 'a1 coq_T -> 'a1 coq_T **)
-  
+
   let seq = fun a k -> (); fun () -> a (); k ()
-  
-  (** val map : ('a1 -> 'a2) -> 'a1 coq_T -> 'a2 coq_T **)
-  
+
   let map = fun f a -> (); fun () -> f (a ())
-  
-  (** val ref : 'a1 -> 'a1 coq_Ref coq_T **)
-  
+
   let ref = fun a -> (); fun () -> Pervasives.ref a
-  
-  (** val set : 'a1 coq_Ref -> 'a1 -> unit coq_T **)
-  
+
   let set = fun r a -> (); fun () -> Pervasives.(:=) r a
-  
-  (** val get : 'a1 coq_Ref -> 'a1 coq_T **)
-  
+
   let get = fun r -> (); fun () -> Pervasives.(!) r
-  
-  (** val raise : exn -> 'a1 coq_T **)
-  
+
   let raise = fun e -> (); fun () -> raise (Proof_errors.Exception e)
-  
-  (** val catch : 'a1 coq_T -> (exn -> 'a1 coq_T) -> 'a1 coq_T **)
-  
+
   let catch = fun s h -> ();
   fun () -> try s ()
   with Proof_errors.Exception e as src ->
     let src = Errors.push src in
     let e = Backtrace.app_backtrace ~src ~dst:e in
     h e ()
-  
-  (** val read_line : string coq_T **)
-  
+
   let read_line = fun () -> try Pervasives.read_line () with e -> let e = Errors.push e in raise e ()
-  
-  (** val print_char : char -> unit coq_T **)
-  
+
   let print_char = fun c -> (); fun () -> print_char c
-  
-  (** val print : Pp.std_ppcmds -> unit coq_T **)
-  
+
   let print = fun s -> (); fun () -> try Pp.pp s; Pp.pp_flush () with e -> let e = Errors.push e in raise e ()
-  
-  (** val timeout : int -> 'a1 coq_T -> 'a1 coq_T **)
-  
+
   let timeout = fun n t -> (); fun () ->
     Control.timeout n t (Proof_errors.Exception Proof_errors.Timeout)
 
@@ -87,84 +52,13 @@ type logicalMessageType = bool*(Goal.goal list*Goal.goal list)
 
 type logicalEnvironment = Environ.env
 
-module NonLogical = 
- struct 
-  type 'a t = 'a IOBase.coq_T
-  
-  type 'a ref = 'a IOBase.coq_Ref
-  
-  (** val ret : 'a1 -> 'a1 t **)
-  
-  let ret x =
-    IOBase.ret x
-  
-  (** val bind : 'a1 t -> ('a1 -> 'a2 t) -> 'a2 t **)
-  
-  let bind x k =
-    IOBase.bind x k
-  
-  (** val ignore : 'a1 t -> unit t **)
-  
-  let ignore x =
-    IOBase.ignore x
-  
-  (** val seq : unit t -> 'a1 t -> 'a1 t **)
-  
-  let seq x k =
-    IOBase.seq x k
-  
-  (** val map : ('a1 -> 'a2) -> 'a1 t -> 'a2 t **)
-  
-  let map f x =
-    (); (IOBase.map f x)
-  
-  (** val new_ref : 'a1 -> 'a1 ref t **)
-  
-  let new_ref x =
-    IOBase.ref x
-  
-  (** val set : 'a1 ref -> 'a1 -> unit t **)
-  
-  let set r x =
-    IOBase.set r x
-  
-  (** val get : 'a1 ref -> 'a1 t **)
-  
-  let get r =
-    IOBase.get r
-  
-  (** val raise : exn -> 'a1 t **)
-  
-  let raise e =
-    IOBase.raise e
-  
-  (** val catch : 'a1 t -> (exn -> 'a1 t) -> 'a1 t **)
-  
-  let catch s h =
-    IOBase.catch s h
-  
-  (** val timeout : int -> 'a1 t -> 'a1 t **)
-  
-  let timeout n x =
-    IOBase.timeout n x
-  
-  (** val read_line : string t **)
-  
-  let read_line =
-    IOBase.read_line
-  
-  (** val print_char : char -> unit t **)
-  
-  let print_char c =
-    IOBase.print_char c
-  
-  (** val print : Pp.std_ppcmds -> unit t **)
-  
-  let print s =
-    IOBase.print s
-  
-  (** val run : 'a1 t -> 'a1 **)
-  
+module NonLogical =
+ struct
+  include IO
+  type 'a ref = 'a IO.coq_Ref
+
+  let new_ref = ref
+
   let run = fun x ->
   try x () with Proof_errors.Exception e as src ->
     let src = Errors.push src in
@@ -172,433 +66,106 @@ module NonLogical =
     Pervasives.raise e
  end
 
-module Logical = 
- struct 
-  type 'a t =
-    __ -> ('a -> proofview -> __ -> (__ -> __ -> (__ -> (bool*(Goal.goal
-    list*Goal.goal list)) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-    IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ ->
-    (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __
-    IOBase.coq_T) -> __ IOBase.coq_T) -> Environ.env -> __ -> (__ ->
-    (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __
-    IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-    IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-    IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-    proofview -> __ -> (__ -> __ -> (__ -> (bool*(Goal.goal list*Goal.goal
-    list)) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-    (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __
-    IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-    IOBase.coq_T) -> Environ.env -> __ -> (__ -> (bool*(Goal.goal
-    list*Goal.goal list)) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-    IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ ->
-    (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __
-    IOBase.coq_T) -> __ IOBase.coq_T
-  
-  (** val ret :
-      'a1 -> __ -> ('a1 -> proofview -> __ -> ('a2 -> __ -> (__ ->
-      (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> (__ -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> proofview -> __ -> ('a2 -> __ -> ('a3 ->
-      (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> ('a3 -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> ('a4 -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> ('a4 -> (exn -> 'a5
-      IOBase.coq_T) -> 'a5 IOBase.coq_T) -> (exn -> 'a5 IOBase.coq_T) -> 'a5
-      IOBase.coq_T **)
-  
-  let ret x =
-    (); (fun _ k s -> Obj.magic k x s)
-  
-  (** val bind :
-      'a1 t -> ('a1 -> 'a2 t) -> __ -> ('a2 -> proofview -> __ -> ('a3 -> __
-      -> (__ -> (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn
-      -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) ->
-      __ IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> (__ -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> proofview -> __ -> ('a3 -> __ -> ('a4 ->
-      (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> ('a4 -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> ('a5 -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> ('a5 -> (exn -> 'a6
-      IOBase.coq_T) -> 'a6 IOBase.coq_T) -> (exn -> 'a6 IOBase.coq_T) -> 'a6
-      IOBase.coq_T **)
-  
-  let bind x k =
-    (); (fun _ k0 s -> Obj.magic x __ (fun a s' -> Obj.magic k a __ k0 s') s)
-  
-  (** val ignore :
-      'a1 t -> __ -> (unit -> proofview -> __ -> ('a2 -> __ -> (__ ->
-      (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> (__ -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> proofview -> __ -> ('a2 -> __ -> ('a3 ->
-      (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> ('a3 -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> ('a4 -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> ('a4 -> (exn -> 'a5
-      IOBase.coq_T) -> 'a5 IOBase.coq_T) -> (exn -> 'a5 IOBase.coq_T) -> 'a5
-      IOBase.coq_T **)
-  
-  let ignore x =
-    (); (fun _ k s -> Obj.magic x __ (fun x1 s' -> k () s') s)
-  
-  (** val seq :
-      unit t -> 'a1 t -> __ -> ('a1 -> proofview -> __ -> ('a2 -> __ -> (__
-      -> (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> (__ -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> proofview -> __ -> ('a2 -> __ -> ('a3 ->
-      (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> ('a3 -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> ('a4 -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> ('a4 -> (exn -> 'a5
-      IOBase.coq_T) -> 'a5 IOBase.coq_T) -> (exn -> 'a5 IOBase.coq_T) -> 'a5
-      IOBase.coq_T **)
-  
-  let seq x k =
-    (); (fun _ k0 s -> Obj.magic x __ (fun x1 s' -> Obj.magic k __ k0 s') s)
-  
-  (** val map :
-      ('a1 -> 'a2) -> 'a1 t -> __ -> ('a2 -> proofview -> __ -> ('a3 -> __ ->
-      (__ -> (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> (__ -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> proofview -> __ -> ('a3 -> __ -> ('a4 ->
-      (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> ('a4 -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> ('a5 -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> ('a5 -> (exn -> 'a6
-      IOBase.coq_T) -> 'a6 IOBase.coq_T) -> (exn -> 'a6 IOBase.coq_T) -> 'a6
-      IOBase.coq_T **)
-  
-  let map f x =
-    (); (fun _ k s -> Obj.magic x __ (fun a s0 -> k (f a) s0) s)
-  
-  (** val set :
-      logicalState -> __ -> (unit -> proofview -> __ -> ('a1 -> __ -> (__ ->
-      (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> (__ -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> proofview -> __ -> ('a1 -> __ -> ('a2 ->
-      (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> ('a2 -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> ('a3 -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> ('a3 -> (exn -> 'a4
-      IOBase.coq_T) -> 'a4 IOBase.coq_T) -> (exn -> 'a4 IOBase.coq_T) -> 'a4
-      IOBase.coq_T **)
-  
-  let set s =
-    (); (fun _ k x -> Obj.magic k () s)
-  
-  (** val get :
-      __ -> (logicalState -> proofview -> __ -> ('a1 -> __ -> (__ ->
-      (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> (__ -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> proofview -> __ -> ('a1 -> __ -> ('a2 ->
-      (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> ('a2 -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> ('a3 -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> ('a3 -> (exn -> 'a4
-      IOBase.coq_T) -> 'a4 IOBase.coq_T) -> (exn -> 'a4 IOBase.coq_T) -> 'a4
-      IOBase.coq_T **)
-  
-  let get r k s =
-    Obj.magic k s s
-  
-  (** val modify :
-      (logicalState -> logicalState) -> __ -> (unit -> proofview -> __ ->
-      ('a1 -> __ -> (__ -> (bool*(Goal.goal list*Goal.goal list)) -> __ ->
-      (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> Environ.env -> __ -> (__ -> (bool*(Goal.goal
-      list*Goal.goal list)) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ ->
-      (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> proofview -> __ -> ('a1 -> __ ->
-      ('a2 -> (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> ('a2 -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> ('a3 -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> ('a3 -> (exn -> 'a4
-      IOBase.coq_T) -> 'a4 IOBase.coq_T) -> (exn -> 'a4 IOBase.coq_T) -> 'a4
-      IOBase.coq_T **)
-  
-  let modify f =
-    (); (fun _ k s -> Obj.magic k () (f s))
-  
-  (** val put :
-      logicalMessageType -> __ -> (unit -> proofview -> __ -> ('a1 -> __ ->
-      (__ -> (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> (__ -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> proofview -> __ -> ('a1 -> __ -> ('a2 ->
-      (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> ('a2 -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> ('a3 -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> ('a3 -> (exn -> 'a4
-      IOBase.coq_T) -> 'a4 IOBase.coq_T) -> (exn -> 'a4 IOBase.coq_T) -> 'a4
-      IOBase.coq_T **)
-  
-  let put m =
-    (); (fun _ k s _ k0 e _ k1 ->
-      Obj.magic k () s __ k0 e __ (fun b c' ->
-        k1 b
-          ((if fst m then fst c' else false),((List.append (fst (snd m))
-                                                (fst (snd c'))),(List.append
-                                                                  (snd
-                                                                    (snd m))
-                                                                  (snd
-                                                                    (snd c')))))))
-  
-  (** val current :
-      __ -> (logicalEnvironment -> proofview -> __ -> ('a1 -> __ -> (__ ->
-      (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> (__ -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> proofview -> __ -> ('a1 -> __ -> ('a2 ->
-      (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> ('a2 -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> ('a3 -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> ('a3 -> (exn -> 'a4
-      IOBase.coq_T) -> 'a4 IOBase.coq_T) -> (exn -> 'a4 IOBase.coq_T) -> 'a4
-      IOBase.coq_T **)
-  
-  let current r k s r0 k0 e =
-    Obj.magic k e s __ k0 e
-  
-  (** val zero :
-      exn -> __ -> ('a1 -> proofview -> __ -> ('a2 -> __ -> (__ ->
-      (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> (__ -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> proofview -> __ -> ('a2 -> __ -> ('a3 ->
-      (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> ('a3 -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> ('a4 -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> ('a4 -> (exn -> 'a5
-      IOBase.coq_T) -> 'a5 IOBase.coq_T) -> (exn -> 'a5 IOBase.coq_T) -> 'a5
-      IOBase.coq_T **)
-  
-  let zero e =
-    (); (fun _ k s _ k0 e0 _ k1 _ sk fk -> fk e)
-  
-  (** val plus :
-      'a1 t -> (exn -> 'a1 t) -> __ -> ('a1 -> proofview -> __ -> ('a2 -> __
-      -> (__ -> (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn
-      -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) ->
-      __ IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> (__ -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> proofview -> __ -> ('a2 -> __ -> ('a3 ->
-      (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> ('a3 -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> ('a4 -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> ('a4 -> (exn -> 'a5
-      IOBase.coq_T) -> 'a5 IOBase.coq_T) -> (exn -> 'a5 IOBase.coq_T) -> 'a5
-      IOBase.coq_T **)
-  
-  let plus x y =
-    (); (fun _ k s _ k0 e _ k1 _ sk fk ->
-      Obj.magic x __ k s __ k0 e __ k1 __ sk (fun e0 ->
-        Obj.magic y e0 __ k s __ k0 e __ k1 __ sk fk))
-  
-  (** val split :
-      'a1 t -> __ -> (('a1, exn -> 'a1 t) list_view -> proofview -> __ ->
-      ('a2 -> __ -> (__ -> (bool*(Goal.goal list*Goal.goal list)) -> __ ->
-      (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> Environ.env -> __ -> (__ -> (bool*(Goal.goal
-      list*Goal.goal list)) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ ->
-      (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> proofview -> __ -> ('a2 -> __ ->
-      ('a3 -> (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> ('a3 -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> ('a4 -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> ('a4 -> (exn -> 'a5
-      IOBase.coq_T) -> 'a5 IOBase.coq_T) -> (exn -> 'a5 IOBase.coq_T) -> 'a5
-      IOBase.coq_T **)
-  
-  let split x =
-    (); (fun _ k s _ k0 e _ k1 _ sk fk ->
-      IOBase.bind
-        (Obj.magic x __ (fun a s' _ k2 e0 -> k2 (a,s')) s __ (fun a _ k2 ->
-          k2 a (true,([],[]))) e __ (fun a c _ sk0 fk0 -> sk0 (a,c) fk0) __
-          (fun a fk0 ->
-          IOBase.ret (Cons (a, (fun e0 _ sk0 fk1 ->
-            IOBase.bind (fk0 e0) (fun x0 ->
-              match x0 with
-              | Nil e1 -> fk1 e1
-              | Cons (a0, x1) -> sk0 a0 (fun e1 -> x1 e1 __ sk0 fk1))))))
-          (fun e0 -> IOBase.ret (Nil e0))) (fun x0 ->
-        match x0 with
-        | Nil exc ->
-          let c = true,([],[]) in
-          Obj.magic k (Nil exc) s __ k0 e __ (fun b c' ->
-            k1 b
-              ((if fst c then fst c' else false),((List.append (fst (snd c))
-                                                    (fst (snd c'))),(List.append
-                                                                    (snd
-                                                                    (snd c))
-                                                                    (snd
-                                                                    (snd c'))))))
-            __ sk fk
-        | Cons (p, y) ->
-          let p0,m' = p in
-          let a',s' = p0 in
-          Obj.magic k (Cons (a', (fun exc _ k2 s0 _ k3 e0 _ k4 _ sk0 fk0 ->
-            y exc __ (fun a fk1 ->
-              let a0,c = a in
-              let a1,s'0 = a0 in
-              k2 a1 s'0 __ k3 e0 __ (fun b c' ->
-                k4 b
-                  ((if fst c then fst c' else false),((List.append
-                                                        (fst (snd c))
-                                                        (fst (snd c'))),
-                  (List.append (snd (snd c)) (snd (snd c')))))) __ sk0 fk1)
-              fk0))) s' __ k0 e __ (fun b c' ->
-            k1 b
-              ((if fst m' then fst c' else false),((List.append
-                                                     (fst (snd m'))
-                                                     (fst (snd c'))),
-              (List.append (snd (snd m')) (snd (snd c')))))) __ sk fk))
-  
-  (** val lift :
-      'a1 NonLogical.t -> __ -> ('a1 -> proofview -> __ -> ('a2 -> __ -> (__
-      -> (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> (__ -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> proofview -> __ -> ('a2 -> __ -> ('a3 ->
-      (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __
-      IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
-      IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
-      Environ.env -> __ -> ('a3 -> (bool*(Goal.goal list*Goal.goal list)) ->
-      __ -> ('a4 -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn ->
-      __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> ('a4 -> (exn -> 'a5
-      IOBase.coq_T) -> 'a5 IOBase.coq_T) -> (exn -> 'a5 IOBase.coq_T) -> 'a5
-      IOBase.coq_T **)
-  
-  let lift x =
-    (); (fun _ k s _ k0 e _ k1 _ sk fk ->
-      IOBase.bind x (fun x0 ->
-        Obj.magic k x0 s __ k0 e __ (fun b c' ->
-          k1 b
-            ((if fst (true,([],[])) then fst c' else false),((List.append
-                                                               (fst
-                                                                 (snd
-                                                                   (true,([],[]))))
-                                                               (fst (snd c'))),
-            (List.append (snd (snd (true,([],[])))) (snd (snd c')))))) __ sk
-          fk))
-  
-  (** val run :
-      'a1 t -> logicalEnvironment -> logicalState ->
-      (('a1*logicalState)*logicalMessageType) NonLogical.t **)
-  
-  let run x e s =
-    Obj.magic x __ (fun a s' _ k e0 -> k (a,s')) s __ (fun a _ k ->
-      k a (true,([],[]))) e __ (fun a c _ sk fk -> sk (a,c) fk) __
-      (fun a x0 -> IOBase.ret a) (fun e0 ->
-      IOBase.raise ((fun e -> Proof_errors.TacticFailure e) e0))
- end
+module Logical =
+ struct
+
+  type rt = logicalEnvironment
+  type wt = logicalMessageType
+  type st = logicalState
+
+  type state = {
+    rstate : rt;
+    wstate : wt;
+    sstate : st;
+  }
+
+  let empty = (true, ([], []))
+
+  let merge (b1, (l1, k1)) (b2, (l2, k2)) = (b1 && b2, (l1 @ l2, k1 @ k2))
 
+  type 'a iolist =
+    { iolist : 'r. (exn -> 'r IO.t) -> ('a -> (exn -> 'r IO.t) -> 'r IO.t) -> 'r IO.t }
+
+  type 'a tactic = state -> ('a * state) iolist
+
+  type 'a t = 'a tactic
+
+  let zero e : 'a tactic = (); fun s ->
+    { iolist = fun nil cons -> nil e }
+
+  let plus m1 m2 : 'a tactic = (); fun s ->
+    let m1 = m1 s in
+    { iolist = fun nil cons -> m1.iolist (fun e -> (m2 e s).iolist nil cons) cons }
+
+  let ret x : 'a tactic = (); fun s ->
+    { iolist = fun nil cons -> cons (x, s) nil }
+
+  let bind (m : 'a tactic) (f : 'a -> 'b tactic) : 'b tactic = (); fun s ->
+    let m = m s in
+    { iolist = fun nil cons -> m.iolist nil (fun (x, s) next -> (f x s).iolist next cons) }
+
+  let seq (m : unit tactic) (f : 'a tactic) : 'a tactic = (); fun s ->
+    let m = m s in
+    { iolist = fun nil cons -> m.iolist nil (fun ((), s) next -> (f s).iolist next cons) }
+
+  let map (f : 'a -> 'b) (m : 'a tactic) : 'b tactic = (); fun s ->
+    let m = m s in
+    { iolist = fun nil cons -> m.iolist nil (fun (x, s) next -> cons (f x, s) next) }
+
+  let ignore (m : 'a tactic) : unit tactic = (); fun s ->
+    let m = m s in
+    { iolist = fun nil cons -> m.iolist nil (fun (_, s) next -> cons ((), s) next) }
+
+  let lift (m : 'a IO.t) : 'a tactic = (); fun s ->
+    { iolist = fun nil cons -> IO.bind m (fun x -> cons (x, s) nil) }
+
+  (** State related *)
+
+  let get : st tactic = (); fun s ->
+    { iolist = fun nil cons -> cons (s.sstate, s) nil }
+
+  let set (sstate : st) : unit tactic = (); fun s ->
+    { iolist = fun nil cons -> cons ((), { s with sstate }) nil }
+
+  let modify (f : st -> st) : unit tactic = (); fun s ->
+    { iolist = fun nil cons -> cons ((), { s with sstate = f s.sstate }) nil }
+
+  let current : rt tactic = (); fun s ->
+    { iolist = fun nil cons -> cons (s.rstate, s) nil }
+
+  let put (w : wt) : unit tactic = (); fun s ->
+    { iolist = fun nil cons -> cons ((), { s with wstate = merge w s.wstate }) nil }
+
+  (** List observation *)
+
+  type 'a reified = ('a, exn -> 'a reified) list_view IO.t
+
+  let rec reflect (m : 'a reified) : 'a iolist =
+    { iolist = fun nil cons ->
+      let next = function
+      | Nil e -> nil e
+      | Cons (x, l) -> cons x (fun e -> (reflect (l e)).iolist nil cons)
+      in
+      IO.bind m next
+    }
+
+  let split (m : 'a tactic) : ('a, exn -> 'a t) list_view tactic = (); fun s ->
+    let m = m s in
+    let rnil e = IO.ret (Nil e) in
+    let rcons p l = IO.ret (Cons (p, l)) in
+    { iolist = fun nil cons ->
+      IO.bind (m.iolist rnil rcons) begin function
+      | Nil e -> cons (Nil e, s) nil
+      | Cons ((x, s), l) ->
+        let l e = (); fun _ -> reflect (l e) in
+        cons (Cons (x, l), s) nil
+      end }
+
+  let run m r s =
+    let s = { wstate = empty; rstate = r; sstate = s } in
+    let m = m s in
+    let nil e = IO.raise (Proof_errors.TacticFailure e) in
+    let cons (x, s) _ = IO.ret ((x, s.sstate), s.wstate) in
+    m.iolist nil cons
+
+ end