Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by extraction.

The goal was to use Coq's partial evaluation capabilities to do manually some
inlining that Ocaml couldn't do. It may be critical as we are defining higher
order combinators in term of others and no inlining means a lot of
unnecessary, short-lived closures built.

With this modification we get back some (but not all) of the loss of performance introduced by threading the monadic type all over the place.
I still have an estimated 15% longer compilation time for Coq.

Makes use of Set Extraction Conservative Types and Set Extraction File Comment
to maintain the relationship between the functions and their types.

Uses an intermediate layer Proofview_monad between Proofview_gen and
Proofview in order to use a hand-written mli to catch potential errors in the
generated file (it uses Extract Constant a lot).

A bug in the extraction of signatures forces to remove the generated
proofview_gen.mli which does not have the correct types.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16981 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 600 insertions, 592 deletions

diff --git a/proofs/monads.ml b/proofs/monads.ml
deleted file mode 100644
index 803715a45..000000000
--- a/proofs/monads.ml
+++ /dev/null
@@ -1,496 +0,0 @@
-module type Type = sig
-  type t
-end
-
-module type S = sig
-  type +'a t
-
-  val return : 'a -> 'a t
-  val bind : 'a t -> ('a -> 'b t) -> 'b t
-  val seq : unit t -> 'a t -> 'a t
-  val ignore : 'a t -> unit t
-(* spiwack: these will suffice for now, if we would use monads more
-   globally, then I would add map/join/List.map and such functions,
-   plus default implementations *)
-end
-
-module type State = sig
-  type s (* type of the state *)
-  include S
-
-  val set : s -> unit t
-  val get : s t
-end
-
-module type Writer = sig
-  type m (* type of the messages *)
-  include S
-
-  val put : m -> unit t
-end
-
-module type IO = sig
-  include S
-
-  type 'a ref
-
-  val ref : 'a -> 'a ref t
-  val (:=) : 'a ref -> 'a -> unit t
-  val (!) : 'a ref -> 'a t
-
-  val raise : exn -> 'a t
-  val catch : 'a t -> (exn -> 'a t) -> 'a t
-
-  (** In the basic IO monad, [timeout n x] acts as [x] unless it runs for more than [n]
-      seconds in which case it raises [IO.Timeout]. *)
-  val timeout : int -> 'a t -> 'a t
-end
-
-module IO : sig
-  include IO
-
-  (** To help distinguish between exceptions raised by the [IO] monad
-      from the one used natively by Coq, the former are wrapped in
-      [Exception]. *)
-  exception Exception of exn
-  (** This exception is used to signal abortion in [timeout] functions. *)
-  exception Timeout
-  (** runs the suspension for its effects *)
-  val run : 'a t -> 'a
-end = struct
-  type 'a t = unit -> 'a
-
-  let run x = x ()
-
-  let return x () = x
-  let bind x k () = k (x ()) ()
-  let seq x k () = x (); k ()
-  let ignore x () = ignore (x ())
-
-  type 'a ref = 'a Pervasives.ref
-
-  let ref x () = Pervasives.ref x
-  let (:=) r x () = Pervasives.(:=) r x
-  let (!) r () = Pervasives.(!) r
-
-  exception Exception of exn
-  let raise e () = raise (Exception e)
-  let catch s h () =
-    try s ()
-    with Exception e -> h e ()
-
-  exception Timeout
-  let timeout n t () =
-    let timeout_handler _ = Pervasives.raise (Exception Timeout) in
-    let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
-    Pervasives.ignore (Unix.alarm n);
-    let restore_timeout () =
-      Pervasives.ignore (Unix.alarm 0);
-      Sys.set_signal Sys.sigalrm psh
-    in
-    try
-      let res = t () in
-      restore_timeout ();
-      res
-    with
-    | e -> restore_timeout (); Pervasives.raise e
-
-  let _ = Errors.register_handler begin function
-    | Timeout -> Errors.errorlabstrm "Monads.IO.timeout" (Pp.str"Timeout!")
-    | Exception e -> Errors.print e
-    | _ -> Pervasives.raise Errors.Unhandled
-  end
-end
-
-(* State monad transformer, adapted from Haskell's StateT *)
-module State (X:Type) (T:S) : sig
-  (* spiwack: it is not essential that both ['a result] and ['a t] be
-     private (or either, for that matter). I just hope it will help
-     catch more programming errors. *)
-  type +'a result = private { result : 'a ; state : X.t }
-  include State with type s = X.t and type +'a t = private X.t -> 'a result T.t
-  (* a function version of the coercion from the private type ['a t].*)
-  val run : 'a t -> s -> 'a result T.t
-  val lift : 'a T.t -> 'a t
-end = struct
-  type s = X.t
-  type 'a result = { result : 'a ; state : s }
-  type 'a t = s -> 'a result T.t
-
-  let run x = x
-  (*spiwack: convenience notation, waiting for ocaml 3.12 *)
-  let (>>=) = T.bind
-  let return x s = T.return { result=x ; state=s }
-  let bind x k s =
-    x s >>= fun { result=a ; state=s } ->
-    k a s
-  let ignore x s =
-    x s >>= fun x' ->
-    T.return { x' with result=() }
-  let seq x t s =
-    (x s) >>= fun x' ->
-    t x'.state
-  let lift x s =
-    x >>= fun a ->
-    T.return { result=a ; state=s }
-
-  let set s _ =
-    T.return { result=() ; state=s }
-  let get s =
-    T.return { result=s ; state=s }
-end
-
-module type Monoid = sig
-  type t
-
-  val zero : t
-  val ( * ) : t -> t -> t
-end
-
-module Writer (M:Monoid) (T:S) : sig
-  include Writer with type +'a t = private ('a*M.t) T.t and type m = M.t
-
-  val lift : 'a T.t -> 'a t
-  (* The coercion from private ['a t] in function form. *)
-  val run : 'a t -> ('a*m) T.t
-end = struct
-
-  type 'a t = ('a*M.t) T.t
-  type m = M.t
-
-  let run x = x
-
-  (*spiwack: convenience notation, waiting for ocaml 3.12 *)
-  let (>>=) = T.bind
-
-  let bind x k = 
-    x >>= fun (a,m) ->
-    k a >>= fun (r,m') ->
-    T.return (r,M.( * ) m m')
-
-  let seq x k =
-    x >>= fun ((),m) ->
-    k >>= fun (r,m') ->
-    T.return (r,M.( * ) m m')
-
-  let return x =
-    T.return (x,M.zero)
-
-  let ignore x =
-    x >>= fun (_,m) ->
-    T.return ((),m)
-
-  let lift x =
-    x >>= fun r ->
-    T.return (r,M.zero)
-
-  let put m =
-    T.return ((),m)
-end
-
-(* Double-continuation backtracking monads are reasonable folklore for
-   "search" implementations (including Tac interactive prover's
-   tactics). Yet it's quite hard to wrap your head around these.  I
-   recommand reading a few times the "Backtracking, Interleaving, and
-   Terminating Monad Transformers" paper by O. Kiselyov, C. Chen,
-   D. Fridman.  The peculiar shape of the monadic type is reminiscent
-   of that of the continuation monad transformer.
-
-   The paper also contains the rational for the [split] abstraction.
-
-   An explanation of how to derive such a monad from mathematical
-   principles can be found in "Kan Extensions for Program
-   Optimisation" by Ralf Hinze.
-
-   One way to think of the [Logic] functor is to imagine ['a
-   Logic(X).t] to represent list of ['a] with an exception at the
-   bottom (leaving the monad-transforming issues aside, as they don't
-   really work well with lists). Each of the element is a valid
-   result, sequentialising with a [f:'a -> 'b t] is done by applying
-   [f] to each element and then flatten the list, [plus] is
-   concatenation, and [split] is pattern-matching. *)
-(* spiwack: I added the primitives from [IO] directly in the [Logic]
-   signature for convenience. It doesn't really make sense, strictly
-   speaking, as they are somewhat deconnected from the semantics of
-   [Logic], but without an appropriate language for composition (some
-   kind of mixins?) I would be going nowhere with a gazillion
-   functors. *)
-module type Logic = sig
-  include IO
-
-  (* [zero] is usually argument free, but Coq likes to explain errors,
-     hence error messages should be carried around. *)
-  val zero : exn -> 'a t
-  val plus : 'a t -> (exn -> 'a t) -> 'a t
-(** Writing (+) for plus and (>>=) for bind, we shall require that
-
-    x+(y+z) = (x+y)+z
-
-    zero+x = x
-
-    x+zero = x
-
-    (x+y)>>=k = (x>>=k)+(y>>=k) *)
-
-  (** [split x] runs [x] until it either fails with [zero e] or finds
-      a result [a].  In the former case it returns [Inr e], otherwise
-      it returns [Inl (a,y)] where [y] can be run to get more results
-      from [x]. It is a variant of prolog's cut. *)
-  val split : 'a t -> ('a * (exn -> 'a t) , exn ) Util.union t
-end
-(* The [T] argument represents the "global" effect: it is not
-   backtracked when backtracking occurs at a [plus]. *)
-(* spiwack: hence, [T] will not be instanciated with a state monad
-   representing the proofs, we will use a surrounding state transformer
-   to that effect. In fact at the time I'm writing this comment, I have
-   no immediate use for [T]. We might, however, consider instantiating it
-   with a "writer" monad around [Pp] to implement [idtac "msg"] for
-   instance. *)
-module Logic (T:IO) : sig
-  include Logic
-
-  (** [run x] raises [e] if [x] is [zero e]. *)
-  val run : 'a t -> 'a T.t
-
-  val lift : 'a T.t -> 'a t
-end = struct
-(* spiwack: the implementation is an adaptation of the aforementionned
-   "Backtracking, Interleaving, and Terminating Monad Transformers"
-   paper *)
-  (* spiwack: [fk] stands for failure continuation, and [sk] for success
-     continuation. *)
-  type +'r fk = exn -> 'r
-  type (-'a,'r) sk = 'a -> 'r fk -> 'r
-  type 'a t = { go : 'r. ('a,'r T.t) sk -> 'r T.t fk -> 'r T.t }
-
-  let return x = { go = fun sk fk ->
-    sk x fk
-                 }
-  let bind x k = { go = fun sk fk ->
-    x.go (fun a fk -> (k a).go sk fk) fk
-                 }
-  let ignore x = { go = fun sk fk ->
-    x.go (fun _ fk -> sk () fk) fk
-                 }
-  let seq x t = { go = fun sk fk ->
-    x.go (fun () fk -> t.go sk fk) fk
-                }
-
-  let zero e = { go = fun _ fk -> fk e }
-
-  let plus x y = { go = fun sk fk ->
-    x.go sk (fun e -> (y e).go sk fk)
-                 }
-
-  let lift x = { go = fun sk fk ->
-    T.bind x (fun a -> sk a fk)
-               }
-
-  let run x =
-    let sk a _ = T.return a in
-    let fk e = raise e in
-    x.go sk fk
-
-  (* For [reflect] and [split] see the "Backtracking, Interleaving,
-     and Terminating Monad Transformers" paper *)
-  let reflect : ('a*(exn -> 'a t) , exn) Util.union -> 'a t = function
-    | Util.Inr e -> zero e
-    | Util.Inl (a,x) -> plus (return a) x
-
-  let lower x =
-    let fk e = T.return (Util.Inr e) in
-    let sk a fk = T.return (Util.Inl (a,fun e -> bind (lift (fk e)) reflect)) in
-    x.go sk fk  
-
-  let split x =
-    lift (lower x)
-
-  (*** IO ***)
-
-  type 'a ref = 'a T.ref
-  let ref x = lift (T.ref x)
-  let (:=) r x = lift (T.(:=) r x)
-  let (!) r = lift (T.(!) r)
-
-  let raise e = lift (T.raise e)
-  let catch t h =
-    let h' e = lower (h e) in
-    bind (lift (T.catch (lower t) h')) reflect
-
-  (** [timeout n x] can have several success. It succeeds as long as,
-      individually, each of the past successes run in less than [n]
-      seconds.
-      In case of timeout if fails with [zero Timeout]. *)
-  let rec timeout n x =
-    (* spiwack: adds a [T.return] in front of [x] in order to force
-       [lower] to go into [T] before running [x]. The problem is that
-       in a continuation-passing monad transformer, the monadic
-       operations don't make use of the underlying ones. Hence, when
-       going back to a lower monad, much computation can be done
-       before returning (and running the lower monad). It is
-       undesirable for timeout, obviously. *)
-    let x = seq (lift (T.return ())) x in
-    let x' =
-      (* spiwack: this could be a [T.map] if provided *)
-      T.bind (lower x) begin function
-        | Util.Inr _ as e -> T.return e
-        | Util.Inl (a,h) -> T.return (Util.Inl (a, fun e -> timeout n (h e)))
-      end
-    in
-    (* spiwack: we report timeouts as resumable failures. *)
-    bind (catch (lift (T.timeout n x')) begin function
-      | IO.Timeout -> zero IO.Timeout
-      | e -> raise e
-    end) reflect
-end
-
-
-(* [State(X)(T:Logic)] can be lifted to [Logic] by backtracking on state on [plus].*)
-module StateLogic(X:Type)(T:Logic) : sig
-  (* spiwack: some duplication from interfaces as we need ocaml 3.12
-     to substitute inside signatures. *)
-  type s = X.t
-  type +'a result = private { result : 'a ; state : s }
-  include Logic with type +'a t = private X.t -> 'a result T.t
-
-  val set : s -> unit t
-  val get : s t
-
-  val lift : 'a T.t -> 'a t
-  val run : 'a t -> s -> 'a result T.t
-end = struct
-
-  module S = State(X)(T)
-  include S
-
-  let zero e = lift (T.zero e)
-  let plus x y =
-    (* spiwack: convenience notation, waiting for ocaml 3.12 *)
-    let (>>=) = bind in
-    let (>>) = seq in
-    get >>= fun initial ->
-    lift begin
-      (T.plus (run x initial) (fun e -> run (y e) initial)) 
-    end >>= fun { result = a ; state = final } ->
-    set final >>
-    return a
-  (* spiwack: the definition of [plus] is essentially [plus x y = fun s
-     -> T.plus (run x s) (run y s)]. But the [private] annotation
-     prevents us from writing that. Maybe I should remove [private]
-     around [+'a t] (it would be unnecessary to remove that of ['a
-     result]) after all. I'll leave it like that for now. *)
-
-  let split x =
-    (* spiwack: convenience notation, waiting for ocaml 3.12 *)
-    let (>>=) = bind in
-    let (>>) = seq in
-    get >>= fun initial ->
-    lift (T.split (run x initial)) >>= function
-      | Util.Inr _ as e -> return e
-      | Util.Inl (a,y) ->
-          let y' e =
-            lift (y e) >>= fun b ->
-            set b.state >>
-            return b.result
-          in
-          set a.state >>
-          return (Util.Inl(a.result,y'))
-
-
-  (*** IO ***)
-
-  type 'a ref = 'a T.ref
-  let ref x = lift (T.ref x)
-  let (:=) r x = lift (T.(:=) r x)
-  let (!) r = lift (T.(!) r)
-
-  let raise e = lift (T.raise e)
-  let catch t h =
-    (* spiwack: convenience notation, waiting for ocaml 3.12 *)
-    let (>>=) = bind in
-    let (>>) = seq in
-    get >>= fun initial ->
-    let h' e = run (h e) initial in
-    lift (T.catch (run t initial) h') >>= fun a ->
-    set a.state >>
-    return a.result
-
-  exception Timeout
-  let timeout n t =
-    (* spiwack: convenience notation, waiting for ocaml 3.12 *)
-    let (>>=) = bind in
-    let (>>) = seq in
-    get >>= fun initial ->
-    lift (T.timeout n (run t initial)) >>= fun a ->
-    set a.state >>
-    return a.result
-end
-
-(* [Writer(M)(T:Logic)] can be lifted to [Logic] by backtracking on state on [plus].*)
-module WriterLogic(M:Monoid)(T:Logic) : sig
-  (* spiwack: some duplication from interfaces as we need ocaml 3.12
-     to substitute inside signatures. *)
-  type m = M.t
-  include Logic with type +'a t = private ('a*m) T.t
-
-  val put : m -> unit t
-
-  val lift : 'a T.t -> 'a t
-  val run : 'a t -> ('a*m) T.t
-end = struct
-  module W = Writer(M)(T)
-  include W
-
-  let zero e = lift (T.zero e)
-  let plus x y =
-    (* spiwack: convenience notation, waiting for ocaml 3.12 *)
-    let (>>=) = bind in
-    let (>>) = seq in
-    lift begin
-      (T.plus (run x) (fun e -> run (y e))) 
-    end >>= fun (r,m) ->
-    put m >>
-    return r
-
-  let split x =
-    (* spiwack: convenience notation, waiting for ocaml 3.12 *)
-    let (>>=) = bind in
-    let (>>) = seq in
-    lift (T.split (run x)) >>= function
-      | Util.Inr _ as e -> return e
-      | Util.Inl ((a,m),y) ->
-          let y' e =
-            lift (y e) >>= fun (b,m) ->
-            put m >>
-            return b
-          in
-          put m >>
-          return (Util.Inl(a,y'))
-
-
-  (*** IO ***)
-
-  type 'a ref = 'a T.ref
-  let ref x = lift (T.ref x)
-  let (:=) r x = lift (T.(:=) r x)
-  let (!) r = lift (T.(!) r)
-
-  let raise e = lift (T.raise e)
-  let catch t h =
-    (* spiwack: convenience notation, waiting for ocaml 3.12 *)
-    let (>>=) = bind in
-    let (>>) = seq in
-    let h' e = run (h e) in
-    lift (T.catch (run t) h') >>= fun (a,m) ->
-    put m >>
-    return a
-
-  exception Timeout
-  let timeout n t =
-    (* spiwack: convenience notation, waiting for ocaml 3.12 *)
-    let (>>=) = bind in
-    let (>>) = seq in
-    lift (T.timeout n (run t)) >>= fun (a,m) ->
-    put m >>
-    return a
-end
diff --git a/proofs/proof_errors.ml b/proofs/proof_errors.ml
new file mode 100644
index 000000000..e543b0c8f
--- /dev/null
+++ b/proofs/proof_errors.ml
@@ -0,0 +1,12 @@
+exception Exception of exn
+exception Timeout
+exception TacticFailure of exn
+
+let _ = Errors.register_handler begin function
+  | Timeout -> Errors.errorlabstrm "Some timeout function" (Pp.str"Timeout!")
+  | Exception e -> Errors.print e
+  | TacticFailure e -> Errors.print e
+  | _ -> Pervasives.raise Errors.Unhandled
+end
+
+
diff --git a/proofs/proof_errors.mli b/proofs/proof_errors.mli
new file mode 100644
index 000000000..dd21d539c
--- /dev/null
+++ b/proofs/proof_errors.mli
@@ -0,0 +1,18 @@
+(** This small files declares the exceptions needed by Proofview_gen,
+    as Coq's extraction cannot produce exception declarations. *)
+
+(** To help distinguish between exceptions raised by the IO monad from
+    the one used natively by Coq, the former are wrapped in
+    [Exception].  It is only used internally so that [catch] blocks of
+    the IO monad would only catch exceptions raised by the [raise]
+    function of the IO monad, and not for instance, by system
+    interrupts. Also used in [Proofview] to avoid capturing exception
+    from the IO monad ([Proofview] catches errors in its compatibility
+    layer, and when lifting goal-level expressions). *)
+exception Exception of exn
+(** This exception is used to signal abortion in [timeout] functions. *)
+exception Timeout
+(** This exception is used by the tactics to signal failure by lack of
+    successes, rather than some other exceptions (like system
+    interrupts). *)
+exception TacticFailure of exn
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 19f289316..4a7efb029 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -1,7 +1,9 @@
 Goal
 Evar_refiner
-Monads
 Proof_type
+Proof_errors
+Proofview_gen
+Proofview_monad
 Proofview
 Proof
 Proof_global
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index eed792fd7..9496b51ea 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -23,11 +23,8 @@
 open Util
 
 (* Type of proofviews. *)
-type proofview = {
-     initial : (Term.constr * Term.types) list;
-     solution : Evd.evar_map;
-     comb : Goal.goal list;
-     }
+type proofview = Proofview_monad.proofview
+open Proofview_monad
 
 let proofview p =
   p.comb , p.solution
@@ -188,79 +185,68 @@ let unfocus c sp =
    - access the environment,
    - access and change the current [proofview]
    - backtrack on previous changes of the proofview *)
-(* spiwack: it seems lighter, for now, to deal with the environment here rather than in [Monads]. *)
-
-module ProofState = struct
-  type t = proofview
-end
-module MessageType = struct
-  type t = bool (* [false] if an unsafe tactic has been used. *)
-
-  let zero = true
-  let ( * ) s1 s2 = s1 && s2
-end
-module Backtrack = Monads.Logic(Monads.IO)
-module Message = Monads.WriterLogic(MessageType)(Backtrack)
-module Proof = Monads.StateLogic(ProofState)(Message)
-
-type +'a tactic = Environ.env -> 'a Proof.t
+module Proof = Proofview_monad.Logical
+type +'a tactic = 'a Proof.t
 
 (* Applies a tactic to the current proofview. *)
 let apply env t sp =
-  let (next,status) = Monads.IO.run (Backtrack.run (Message.run (Proof.run (t env) sp))) in
-  next.Proof.result , next.Proof.state , status
+  let (((next_r,next_state),status)) = Proofview_monad.NonLogical.run (Proof.run t env sp) in
+  next_r , next_state , status
 
 (*** tacticals ***)
 
 
+let rec catchable_exception = function
+  | Proof_errors.Exception _ -> false
+  | e -> Errors.noncritical e
+
+
 (* Unit of the tactic monad *)
-let tclUNIT a _ = Proof.return a
+let tclUNIT a = (Proof.ret a:'a Proof.t)
 
 (* Bind operation of the tactic monad *)
-let tclBIND t k env =
-  Proof.bind (t env) (fun a -> k a env)
+let tclBIND = Proof.bind
 
 (* Interpretes the ";" (semicolon) of Ltac.
    As a monadic operation, it's a specialized "bind"
    on unit-returning tactic (meaning "there is no value to bind") *)
-let tclTHEN t1 t2 env =
-  Proof.seq (t1 env) (t2 env)
+let tclTHEN = Proof.seq
 
 (* [tclIGNORE t] has the same operational content as [t],
    but drops the value at the end. *)
-let tclIGNORE tac env = Proof.ignore (tac env)
+let tclIGNORE = Proof.ignore
 
 (* [tclOR t1 t2 = t1] as long as [t1] succeeds. Whenever the successes
    of [t1] have been depleted and it failed with [e], then it behaves
    as [t2 e].  No interleaving at this point. *)
-let tclOR t1 t2 env =
-  Proof.plus (t1 env) (fun e -> t2 e env)
+let tclOR t1 t2 =
+  Proof.plus t1 t2
 
 (* [tclZERO e] always fails with error message [e]*)
-let tclZERO e _ = Proof.zero e
+let tclZERO = Proof.zero
 
 (* [tclORELSE t1 t2] behaves like [t1] if [t1] succeeds at least once
    or [t2] if [t1] fails. *)
-let tclORELSE t1 t2 env =
+let tclORELSE t1 t2 =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
-  Proof.split (t1 env) >>= function
-    | Util.Inr e -> t2 e env
-    | Util.Inl (a,t1') -> Proof.plus (Proof.return a) t1'
+  Proof.split t1 >>= function
+    | Util.Inr e -> t2 e
+    | Util.Inl (a,t1') -> Proof.plus (Proof.ret a) t1'
 
 (* [tclIFCATCH a s f] is a generalisation of [tclORELSE]: if [a]
    succeeds at least once then it behaves as [tclBIND a s] otherwise, if [a]
    fails with [e], then it behaves as [f e]. *)
-let tclIFCATCH a s f env =
+let tclIFCATCH a s f =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
-  Proof.split (a env) >>= function
-    | Util.Inr e -> f e env
-    | Util.Inl (x,a') -> Proof.plus (s x env) (fun e -> (a' e) >>= fun x' -> (s x' env))
+  Proof.split a >>= function
+    | Util.Inr e -> f e
+    | Util.Inl (x,a') -> Proof.plus (s x) (fun e -> (a' e) >>= fun x' -> (s x'))
 
 (* Focuses a tactic at a range of subgoals, found by their indices. *)
 (* arnaud: bug if 0 goals ! *)
-let tclFOCUS i j t env =
+let tclFOCUS i j t =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
   let (>>) = Proof.seq in
@@ -268,14 +254,14 @@ let tclFOCUS i j t env =
   try
     let (focused,context) = focus i j initial in
     Proof.set focused >>
-    t (env) >>= fun result ->
+    t >>= fun result ->
     Proof.get >>= fun next ->
     Proof.set (unfocus context next) >>
-    Proof.return result
+    Proof.ret result
   with e ->
     (* spiwack: a priori the only possible exceptions are that of focus,
        of course I haven't made them algebraic yet. *)
-    tclZERO e env
+    tclZERO e
 
 (* Dispatch tacticals are used to apply a different tactic to each goal under
    consideration. They come in two flavours:
@@ -299,27 +285,27 @@ end
    both lists are being concatenated.
    [join] and [null] need be some sort of comutative monoid. *)
 
-let rec tclDISPATCHGEN null join tacs env =
+let rec tclDISPATCHGEN null join tacs =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
   let (>>) = Proof.seq in
   Proof.get >>= fun initial ->
   match tacs,initial.comb with
-  | [], [] -> tclUNIT null env
+  | [], [] -> tclUNIT null
   | t::tacs , first::goals ->
       begin match Goal.advance initial.solution first with
-      | None -> Proof.return null (* If [first] has been solved by side effect: do nothing. *)
+      | None -> Proof.ret null (* If [first] has been solved by side effect: do nothing. *)
       | Some first ->
           Proof.set {initial with comb=[first]} >>
-          t env
+          t
       end >>= fun y ->
       Proof.get >>= fun step ->
       Proof.set {step with comb=goals} >>
-      tclDISPATCHGEN null join tacs env >>= fun x ->
+      tclDISPATCHGEN null join tacs >>= fun x ->
       Proof.get >>= fun step' ->
       Proof.set {step' with comb=step.comb@step'.comb} >>
-      Proof.return (join y x)
-  | _ , _ -> tclZERO SizeMismatch env
+      Proof.ret (join y x)
+  | _ , _ -> tclZERO SizeMismatch
 
 let unitK () () = ()
 let tclDISPATCH = tclDISPATCHGEN () unitK
@@ -343,12 +329,12 @@ let extend_to_list =
     let ne = List.length endxs in
     let n = List.length l in
     startxs@(copy (n-ne-ns) rx endxs)
-let tclEXTEND tacs1 rtac tacs2 env =
+let tclEXTEND tacs1 rtac tacs2 =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
   Proof.get >>= fun step ->
   let tacs = extend_to_list tacs1 rtac tacs2 step.comb in
-  tclDISPATCH tacs env
+  tclDISPATCH tacs
 
 
 (* No backtracking can happen here, hence, as opposed to the dispatch tacticals,
@@ -367,44 +353,79 @@ let sensitive_on_proofview s env step =
   { step with
      solution = new_defs;
      comb = List.flatten combed_subgoals; }
-  let tclSENSITIVE s env =
+let tclSENSITIVE s =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
+  Proof.current >>= fun env ->
   Proof.get >>= fun step ->
   try
     let next = sensitive_on_proofview s env step in
     Proof.set next
-  with e when Errors.noncritical e ->
-    tclZERO e env
+  with e when catchable_exception e ->
+    tclZERO e
 
-let tclPROGRESS t env =
+let tclPROGRESS t =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
   Proof.get >>= fun initial ->
-  t env >>= fun res ->
+  t >>= fun res ->
   Proof.get >>= fun final ->
   let test =
     Evd.progress_evar_map initial.solution final.solution &&
     not (Util.List.for_all2eq (fun i f -> Goal.equal initial.solution i final.solution f) initial.comb final.comb)
   in
   if test then
-    tclUNIT res env
+    tclUNIT res
   else
-    tclZERO (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) env
+    tclZERO (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress."))
 
-let tclEVARMAP _ =
+let tclEVARMAP =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
   Proof.get >>= fun initial ->
-  Proof.return (initial.solution)
+  Proof.ret (initial.solution)
 
-let tclENV env =
-  Proof.return env
+let tclENV = Proof.current
 
-let tclTIMEOUT n t env = Proof.timeout n (t env)
+exception Timeout
+let _ = Errors.register_handler begin function
+  | Timeout -> Errors.errorlabstrm "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
+  | _ -> Pervasives.raise Errors.Unhandled
+end
 
-let mark_as_unsafe env =
-  Proof.lift (Message.put false)
+let tclTIMEOUT n t =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Proof.bind in
+  let (>>) = Proof.seq in
+  (* spiwack: as one of the monad is a continuation passing monad, it
+     doesn't force the computation to be threaded inside the underlying
+     (IO) monad. Hence I force it myself by asking for the evaluation of
+     a dummy value first, lest [timeout] be called when everything has
+     already been computed. *)
+  let t = Proof.lift (Proofview_monad.NonLogical.ret ()) >> t in
+  Proof.current >>= fun env ->
+  Proof.get >>= fun initial ->
+  Proof.lift begin
+    Proofview_monad.NonLogical.catch
+      begin
+        Proofview_monad.NonLogical.bind
+          (Proofview_monad.NonLogical.timeout n (Proof.run t env initial))
+          (fun r -> Proofview_monad.NonLogical.ret (Util.Inl r))
+      end
+      begin function
+        | Proof_errors.Timeout -> Proofview_monad.NonLogical.ret (Util.Inr Timeout)
+        | Proof_errors.TacticFailure e -> Proofview_monad.NonLogical.ret (Util.Inr e)
+        | e -> Proofview_monad.NonLogical.raise e
+      end
+  end >>= function
+    | Util.Inl ((res,s),m) ->
+        Proof.set s >>
+        Proof.put m >>
+        Proof.ret res
+    | Util.Inr e -> tclZERO e
+
+let mark_as_unsafe =
+  Proof.put false
 
 (*** Commands ***)
 
@@ -430,7 +451,7 @@ module Notations = struct
     end >= fun l' ->
     tclUNIT (List.flatten l')
   let (<*>) = tclTHEN
-  let (<+>) t1 t2 = tclOR t2 (fun _ -> t2)
+  let (<+>) t1 t2 = tclOR t1 (fun _ -> t2)
 end
 
 open Notations
@@ -446,7 +467,7 @@ let rec list_map f = function
 module V82 = struct
   type tac = Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
-  let tactic tac env =
+  let tactic tac =
     (* spiwack: we ignore the dependencies between goals here, expectingly
        preserving the semantics of <= 8.2 tactics *)
     (* spiwack: convenience notations, waiting for ocaml 3.12 *)
@@ -467,8 +488,8 @@ module V82 = struct
       let (goalss,evd) = Goal.list_map tac initgoals initevd in
       let sgs = List.flatten goalss in
       Proof.set { ps with solution=evd ; comb=sgs; }
-    with e when Errors.noncritical e ->
-      tclZERO e env
+    with e when catchable_exception e ->
+      tclZERO e
 
   let has_unresolved_evar pv =
     Evd.has_undefined pv.solution
@@ -515,14 +536,16 @@ module V82 = struct
 	solution = Evar_refiner.instantiate_pf_com evk com pv.solution }
 
   let of_tactic t gls =
-    let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] ; initial = [] } in
-    let (_,final,_) = apply (Goal.V82.env gls.Evd.sigma gls.Evd.it) t init in
-    { Evd.sigma = final.solution ; it = final.comb }
+    try
+      let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] ; initial = [] } in
+      let (_,final,_) = apply (Goal.V82.env gls.Evd.sigma gls.Evd.it) t init in
+      { Evd.sigma = final.solution ; it = final.comb }
+    with Proof_errors.TacticFailure e -> raise e
 
-  let put_status b _env =
-    Proof.lift (Message.put b)
+  let put_status b =
+    Proof.put b
 
-  let catchable_exception = Errors.noncritical
+  let catchable_exception = catchable_exception
 end
 
 
@@ -530,10 +553,11 @@ module Goal = struct
 
   type 'a u = 'a list
 
-  let lift s env =
+  let lift s =
     (* spiwack: convenience notations, waiting for ocaml 3.12 *)
     let (>>=) = Proof.bind in
     let (>>) = Proof.seq in
+    Proof.current >>= fun env ->
     Proof.get >>= fun step ->
     try
       let (res,sigma) =
@@ -542,22 +566,12 @@ module Goal = struct
         end step.comb step.solution
       in
       Proof.set { step with solution=sigma } >>
-        Proof.return res
-    with e when Errors.noncritical e ->
-      tclZERO e env
+        Proof.ret res
+    with e when catchable_exception e ->
+      tclZERO e
 
   let return x = lift (Goal.return x)
   let concl = lift Goal.concl
   let hyps = lift Goal.hyps
   let env = lift Goal.env
 end
-
-
-
-
-
-
-
-
-
-
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index a2a574693..136a44332 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -194,10 +194,9 @@ val tclEVARMAP : Evd.evar_map tactic
    environment is returned by {!Proofview.Goal.env}. *)
 val tclENV : Environ.env tactic
 
-(** [tclTIMEOUT n t] can have several success. It succeeds as long as,
-      individually, each of the past successes run in less than [n]
-      seconds.
-      In case of timeout if fails with [tclZERO Timeout]. *)
+exception Timeout
+(** [tclTIMEOUT n t] can have only one success.
+    In case of timeout if fails with [tclZERO Timeout]. *)
 val tclTIMEOUT : int -> 'a tactic -> 'a tactic
 
 (** [mark_as_unsafe] signals that the current tactic is unsafe. *)
diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml
new file mode 100644
index 000000000..577aa2ddb
--- /dev/null
+++ b/proofs/proofview_gen.ml
@@ -0,0 +1,377 @@
+(* This file has been generated by extraction
+   of bootstrap/Monad.v. It shouldn't be
+   modified directly. To regenerate it run
+   coqtop -batch -impredicative-set
+   bootstrap/Monad.v in Coq's source
+   directory. *)
+
+type __ = Obj.t
+let __ = let rec f _ = Obj.repr f in Obj.repr f
+
+module IOBase = 
+ struct 
+  type 'a coq_T = unit -> 'a
+  
+  type 'a coq_Ref = 'a Pervasives.ref
+  
+  (** val ret : 'a1 -> 'a1 coq_T **)
+  
+  let ret = fun a () -> a
+  
+  (** val bind :
+      'a1 coq_T -> ('a1 -> 'a2 coq_T) -> 'a2
+      coq_T **)
+  
+  let bind = fun a k () -> k (a ()) ()
+  
+  (** val ignore :
+      'a1 coq_T -> unit coq_T **)
+  
+  let ignore = fun a () -> ignore (a ())
+  
+  (** val seq :
+      unit coq_T -> 'a1 coq_T -> 'a1 coq_T **)
+  
+  let seq = fun a k () -> a (); k ()
+  
+  (** val ref : 'a1 -> 'a1 coq_Ref coq_T **)
+  
+  let ref = fun a () -> Pervasives.ref a
+  
+  (** val set :
+      'a1 coq_Ref -> 'a1 -> unit coq_T **)
+  
+  let set = fun r a () -> Pervasives.(:=) r a
+  
+  (** val get : 'a1 coq_Ref -> 'a1 coq_T **)
+  
+  let get = fun r () -> Pervasives.(!) r
+  
+  (** val raise : exn -> 'a1 coq_T **)
+  
+  let raise = fun e () -> raise (Proof_errors.Exception e)
+  
+  (** val catch :
+      'a1 coq_T -> (exn -> 'a1 coq_T) -> 'a1
+      coq_T **)
+  
+  let catch = fun s h () -> try s () with Proof_errors.Exception e -> h e ()
+  
+  type coq_Int = int
+  
+  (** val timeout :
+      coq_Int -> 'a1 coq_T -> 'a1 coq_T **)
+  
+  let timeout = fun n t () ->
+    let timeout_handler _ = Pervasives.raise (Proof_errors.Exception Proof_errors.Timeout) in
+    let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
+    Pervasives.ignore (Unix.alarm n);
+    let restore_timeout () =
+      Pervasives.ignore (Unix.alarm 0);
+      Sys.set_signal Sys.sigalrm psh
+    in
+    try
+      let res = t () in
+      restore_timeout ();
+      res
+    with
+    | e -> restore_timeout (); Pervasives.raise e
+ 
+ end
+
+type proofview = { initial : (Term.constr*Term.types)
+                             list;
+                   solution : Evd.evar_map;
+                   comb : Goal.goal list }
+
+type logicalState = proofview
+
+type logicalMessageType = bool
+
+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 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 :
+      IOBase.coq_Int -> 'a1 t -> 'a1 t **)
+  
+  let timeout n x =
+    IOBase.timeout n x
+  
+  (** val run : 'a1 t -> 'a1 **)
+  
+  let run = fun x -> try x () with Proof_errors.Exception e -> Pervasives.raise e
+ end
+
+module Logical = 
+ struct 
+  type 'a t =
+    proofview -> Environ.env -> __ ->
+    ((('a*proofview)*bool) -> (exn -> __
+    IOBase.coq_T) -> __ IOBase.coq_T) -> (exn
+    -> __ IOBase.coq_T) -> __ IOBase.coq_T
+  
+  (** val ret :
+      'a1 -> proofview -> Environ.env -> __
+      -> ((('a1*proofview)*bool) -> (exn ->
+      'a2 IOBase.coq_T) -> 'a2 IOBase.coq_T)
+      -> (exn -> 'a2 IOBase.coq_T) -> 'a2
+      IOBase.coq_T **)
+  
+  let ret x s e r sk fk =
+    sk ((x,s),true) fk
+  
+  (** val bind :
+      'a1 t -> ('a1 -> 'a2 t) -> proofview ->
+      Environ.env -> __ ->
+      ((('a2*proofview)*bool) -> (exn -> 'a3
+      IOBase.coq_T) -> 'a3 IOBase.coq_T) ->
+      (exn -> 'a3 IOBase.coq_T) -> 'a3
+      IOBase.coq_T **)
+  
+  let bind x k s e r sk fk =
+    Obj.magic x s e __ (fun a fk0 ->
+      let x0,c = a in
+      let x1,s0 = x0 in
+      Obj.magic k x1 s0 e __ (fun a0 fk1 ->
+        let y,c' = a0 in
+        sk (y,(if c then c' else false)) fk1)
+        fk0) fk
+  
+  (** val ignore :
+      'a1 t -> proofview -> Environ.env -> __
+      -> (((unit*proofview)*bool) -> (exn ->
+      'a2 IOBase.coq_T) -> 'a2 IOBase.coq_T)
+      -> (exn -> 'a2 IOBase.coq_T) -> 'a2
+      IOBase.coq_T **)
+  
+  let ignore x s e r sk fk =
+    Obj.magic x s e __ (fun a fk0 ->
+      let x0,c = a in
+      let sk0 = fun a0 fk1 ->
+        let y,c' = a0 in
+        sk (y,(if c then c' else false)) fk1
+      in
+      let a0,s0 = x0 in
+      sk0 (((),s0),true) fk0) fk
+  
+  (** val seq :
+      unit t -> 'a1 t -> proofview ->
+      Environ.env -> __ ->
+      ((('a1*proofview)*bool) -> (exn -> 'a2
+      IOBase.coq_T) -> 'a2 IOBase.coq_T) ->
+      (exn -> 'a2 IOBase.coq_T) -> 'a2
+      IOBase.coq_T **)
+  
+  let seq x k s e r sk fk =
+    Obj.magic x s e __ (fun a fk0 ->
+      let x0,c = a in
+      let u,s0 = x0 in
+      Obj.magic k s0 e __ (fun a0 fk1 ->
+        let y,c' = a0 in
+        sk (y,(if c then c' else false)) fk1)
+        fk0) fk
+  
+  (** val set :
+      logicalState -> proofview ->
+      Environ.env -> __ ->
+      (((unit*proofview)*bool) -> (exn -> 'a1
+      IOBase.coq_T) -> 'a1 IOBase.coq_T) ->
+      (exn -> 'a1 IOBase.coq_T) -> 'a1
+      IOBase.coq_T **)
+  
+  let set s s0 e r sk fk =
+    sk (((),s),true) fk
+  
+  (** val get :
+      proofview -> Environ.env -> __ ->
+      (((logicalState*proofview)*bool) ->
+      (exn -> 'a1 IOBase.coq_T) -> 'a1
+      IOBase.coq_T) -> (exn -> 'a1
+      IOBase.coq_T) -> 'a1 IOBase.coq_T **)
+  
+  let get s e r sk fk =
+    sk ((s,s),true) fk
+  
+  (** val put :
+      logicalMessageType -> proofview ->
+      Environ.env -> __ ->
+      (((unit*proofview)*bool) -> (exn -> 'a1
+      IOBase.coq_T) -> 'a1 IOBase.coq_T) ->
+      (exn -> 'a1 IOBase.coq_T) -> 'a1
+      IOBase.coq_T **)
+  
+  let put m s e r sk fk =
+    sk (((),s),m) fk
+  
+  (** val current :
+      proofview -> Environ.env -> __ ->
+      (((logicalEnvironment*proofview)*bool)
+      -> (exn -> 'a1 IOBase.coq_T) -> 'a1
+      IOBase.coq_T) -> (exn -> 'a1
+      IOBase.coq_T) -> 'a1 IOBase.coq_T **)
+  
+  let current s e r sk fk =
+    sk ((e,s),true) fk
+  
+  (** val zero :
+      exn -> proofview -> Environ.env -> __
+      -> ((('a1*proofview)*bool) -> (exn ->
+      'a2 IOBase.coq_T) -> 'a2 IOBase.coq_T)
+      -> (exn -> 'a2 IOBase.coq_T) -> 'a2
+      IOBase.coq_T **)
+  
+  let zero e s e0 r sk fk =
+    fk e
+  
+  (** val plus :
+      'a1 t -> (exn -> 'a1 t) -> proofview ->
+      Environ.env -> __ ->
+      ((('a1*proofview)*bool) -> (exn -> 'a2
+      IOBase.coq_T) -> 'a2 IOBase.coq_T) ->
+      (exn -> 'a2 IOBase.coq_T) -> 'a2
+      IOBase.coq_T **)
+  
+  let plus x y s env r sk fk =
+    Obj.magic x s env __ sk (fun e ->
+      Obj.magic y e s env __ sk fk)
+  
+  (** val split :
+      'a1 t -> proofview -> Environ.env -> __
+      -> (((('a1*(exn -> 'a1 t), exn)
+      Util.union*proofview)*bool) -> (exn ->
+      'a2 IOBase.coq_T) -> 'a2 IOBase.coq_T)
+      -> (exn -> 'a2 IOBase.coq_T) -> 'a2
+      IOBase.coq_T **)
+  
+  let split x s e r sk fk =
+    IOBase.bind
+      (Obj.magic x s e __ (fun a fk0 ->
+        IOBase.ret (Util.Inl
+          (a,(fun e0 _ sk0 fk1 ->
+          IOBase.bind (fk0 e0) (fun x0 ->
+            match x0 with
+            | Util.Inl p ->
+              let a0,x1 = p in
+              sk0 a0 (fun e1 ->
+                x1 e1 __ sk0 fk1)
+            | Util.Inr e1 -> fk1 e1)))))
+        (fun e0 -> IOBase.ret (Util.Inr e0)))
+      (fun x0 ->
+      let sk0 = fun a fk0 ->
+        let sk0 = fun a0 fk1 ->
+          let x1,c = a0 in
+          let sk0 = fun a1 fk2 ->
+            let y,c' = a1 in
+            sk (y,(if c then c' else false))
+              fk2
+          in
+          (match x1 with
+           | Util.Inl p ->
+             let p0,y = p in
+             let a1,s0 = p0 in
+             sk0 (((Util.Inl
+               (a1,(fun e0 x2 ->
+               y e0))),s0),true) fk1
+           | Util.Inr e0 ->
+             sk0 (((Util.Inr e0),s),true) fk1)
+        in
+        let x1,c = a in
+        let sk1 = fun a0 fk1 ->
+          let y,c' = a0 in
+          sk0 (y,(if c then c' else false))
+            fk1
+        in
+        (match x1 with
+         | Util.Inl p ->
+           let a0,y = p in
+           sk1 ((Util.Inl (a0,(fun e0 x2 ->
+             y e0))),true) fk0
+         | Util.Inr e0 ->
+           sk1 ((Util.Inr e0),true) fk0)
+      in
+      (match x0 with
+       | Util.Inl p ->
+         let p0,y = p in
+         let a,c = p0 in
+         sk0 ((Util.Inl (a,y)),c) fk
+       | Util.Inr e0 ->
+         sk0 ((Util.Inr e0),true) fk))
+  
+  (** val lift :
+      'a1 NonLogical.t -> proofview ->
+      Environ.env -> __ ->
+      ((('a1*proofview)*bool) -> (exn -> 'a2
+      IOBase.coq_T) -> 'a2 IOBase.coq_T) ->
+      (exn -> 'a2 IOBase.coq_T) -> 'a2
+      IOBase.coq_T **)
+  
+  let lift x s e r sk fk =
+    IOBase.bind x (fun x0 ->
+      sk ((x0,s),true) fk)
+  
+  (** val run :
+      'a1 t -> logicalEnvironment ->
+      logicalState ->
+      (('a1*logicalState)*logicalMessageType)
+      NonLogical.t **)
+  
+  let run x e s =
+    Obj.magic x s e __ (fun a x0 ->
+      IOBase.ret a) (fun e0 ->
+      IOBase.raise
+        ((fun e -> Proof_errors.TacticFailure e)
+          e0))
+ end
+
diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml
new file mode 100644
index 000000000..ebbb04087
--- /dev/null
+++ b/proofs/proofview_monad.ml
@@ -0,0 +1 @@
+include Proofview_gen
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli
new file mode 100644
index 000000000..02550aebc
--- /dev/null
+++ b/proofs/proofview_monad.mli
@@ -0,0 +1,81 @@
+(* This is an interface for the code extracted from bootstrap/Monad.v.
+   The relevant comments are overthere. *)
+
+
+type proofview = { initial : (Term.constr * Term.types) list;
+                   solution : Evd.evar_map; comb : Goal.goal list }
+
+type logicalState = proofview
+
+type logicalEnvironment = Environ.env
+
+type logicalMessageType = bool
+
+
+
+module NonLogical : sig
+
+  type +'a t
+  type 'a ref
+
+  val ret : 'a -> 'a t
+  val bind : 'a t -> ('a -> 'b t) -> 'b t
+  val ignore : 'a t -> unit t
+  val seq : unit t -> 'a t -> 'a t
+
+  val new_ref : 'a -> 'a ref t
+  val set : 'a ref -> 'a -> unit t
+  val get : 'a ref -> 'a t
+
+  val raise : exn -> 'a t
+  val catch : 'a t -> (exn -> 'a t) -> 'a t
+  val timeout : int -> 'a t -> 'a t
+
+
+  (* [run] performs effects. *)
+  val run : 'a t -> 'a
+
+end
+
+
+module Logical : sig
+
+  type +'a t
+
+  val ret : 'a -> 'a t
+  val bind : 'a t -> ('a -> 'b t) -> 'b t
+  val ignore : 'a t -> unit t
+  val seq : unit t -> 'a t -> 'a t
+
+  val set : logicalState -> unit t
+  val get : logicalState t
+  val put : logicalMessageType -> unit t
+  val current : logicalEnvironment t
+
+  val zero : exn -> 'a t
+  val plus : 'a t -> (exn -> 'a t) -> 'a t
+  val split : 'a t -> (('a*(exn->'a t),exn) Util.union) t
+
+  val lift : 'a NonLogical.t -> 'a t
+
+  val run : 'a t -> logicalEnvironment -> logicalState -> (('a*logicalState)*logicalMessageType) NonLogical.t
+end
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+