Cleaning of the new implementation of the tactic monad.

* Add comments in the code (mostly imported from Monad.v)
* Inline duplicated module
* Clean up some artifacts due to the extracted code.
* [NonLogical.new_ref] -> [NonLogical.ref] (I don't even remember why I chose this name originally)
* Remove the now superfluous [Proof_errors] module (which was used to define exceptions to be used in the extracted code).
* Remove Monad.v

11 files changed, 195 insertions, 804 deletions

diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
deleted file mode 100644
index d0412827b1..0000000000
--- a/bootstrap/Monads.v
+++ /dev/null
@@ -1,714 +0,0 @@
-(* -*- coq-prog-args: ("-emacs-U" "-impredicative-set") -*- *)
-
-Reserved Notation "'do' M x ':=' e 'in' u" (at level 200, M at level 0, x ident, e at level 200, u at level 200).
-(*Reserved Notation "'do' e ; u" (at level 200, e at level 200, u at level 200).*)
-
-(*** Unit ***)
-
-Extract Inductive unit => unit [
-  "()"
-].
-Notation "()" := tt.
-
-(*** Bool ***)
-Extract Inductive bool => bool [
-  "true"
-  "false"
-].
-
-(*** List ***)
-Extract Inductive list => list [
-  "[]"
-  "(::)"
-].
-Opaque app.
-Extraction Implicit app [A].
-Extract Inlined Constant app => "List.append".
-
-(*** Prod ***)
-Extract Inductive prod => "(*)" [
-  "(,)"
-].
-Opaque fst.
-Extraction Implicit fst [A B].
-Extract Inlined Constant fst => "fst".
-Extraction Implicit snd [A B].
-Opaque snd.
-Extract Inlined Constant snd => "snd".
-
-
-(*** Closure elimination **)
-
-(* [freeze] is used to help OCaml figure where partial applications
-   are usually made. This way, the compiler will output code optimised
-   for partial applications to happen at this point. It happens to
-   make the monadic code substantially faster.
-
-   Documentation on that particular behaviour can be found at:
-   https://ocaml.janestreet.com/?q=node/30
-*)
-
-Parameter freeze : forall (A : Set), A -> A.
-Extraction Implicit freeze [A].
-Extract Inlined Constant freeze => "();".
-
-(*** Exceptions ***)
-
-Parameter Exception : Set.
-Extract Inlined Constant Exception => exn.
-
-Parameter tactic_failure : Exception -> Exception.
-Extract Inlined Constant tactic_failure => "(fun e -> Proof_errors.TacticFailure e)".
-
-(*** Basic integers ***)
-
-Parameter Int : Set.
-Extract Inlined Constant Int => int.
-
-(*** Char ***)
-
-Parameter Char : Set.
-Extract Inlined Constant Char => char.
-
-(*** Primitive strings ***)
-
-Parameter String : Set.
-Extract Inlined Constant String => string.
-
-(*** Pretty printer ***)
-
-Parameter Ppcmds : Set.
-Extract Inlined Constant Ppcmds => "Pp.std_ppcmds".
-
-(*** A view datatype for the [split] primitive ***)
-
-Inductive list_view (A B:Set) : Set :=
-| Nil : Exception -> list_view A B
-| Cons : A -> B -> list_view A B
-.
-
-(*** Monoids ***)
-
-Module Monoid.
-
-Record T (M:Set) := {
-  zero : M;
-  prod : M -> M -> M
-}.
-
-(** Cartesian product of monoids *)
-Definition cart {M₁} (Mon₁:T M₁) {M₂} (Mon₂:T M₂) : T (M₁*M₂) := {|
-  zero := (Mon₁.(zero _),Mon₂.(zero _));
-  prod x y := (Mon₁.(prod _) (fst x) (fst y), Mon₂.(prod _) (snd x) (snd y))
-|}.
-
-Definition BoolAnd : T bool := {|
-  zero := true;
-  prod := andb
-|}.
-
-Definition List {A:Set} : T (list A) := {|
-  zero := nil ;
-  prod := @app _
-|}.
-
-End Monoid.
-
-(*** Monads and related interfaces ***)
-(* spiwack: the interfaces are presented in a mixin style.
-   I haven't tested other presentation, it just felt
-   convenient when I started *)
-
-Record Monad (T:Set->Set) := {
-  ret : forall{A:Set}, A->T A;
-  bind : forall{A B:Set}, T A -> (A -> T B) -> T B;
-  ignore : forall{A:Set}, T A -> T unit;
-  seq : forall{A:Set}, T unit -> T A -> T A;
-  map : forall {A B : Set}, (A -> B) -> T A -> T B
-}.
-
-Notation "'do' M x ':=' e 'in' u" := (bind _ M e (fun x => u)).
-
-Record State (S:Set) (T:Set->Set) := {
-  set : S -> T unit;
-  get : T S ;
-  modify : (S -> S) -> T unit
-}.
-
-(* spiwack: Environment and Writer are given distinct interfaces from
-   State (rather than state beeing the composition of these) because I
-   don't really know how to combine the three together. However, we
-   might want to be able to arrange things so that we can say "I have a
-   number of things I can get, and a number of things I can set, some
-   of which can be got, and the other being monoids, then I have a
-   monad". I have yet to find how to do that though.*)
-Record Environment (E:Set) (T:Set->Set) := { current : T E }.
-
-Record Writer (M:Set) (T:Set->Set) := {
-  put : M -> T unit
-}.
-
-Record Logic (T:Set -> Set) := {
-  (* [zero] is usually argument free, but Coq likes to explain errors,
-     hence error messages should be carried around. *)
-  zero : forall {A}, Exception -> T A;
-  plus : forall {A}, T A -> (Exception -> T A) -> T A
-}.
-(** 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) *)
-(* 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. [T] is meant to be instantiated with [IO]. *)
-
-
-Module Id.
-
- Definition M : Monad (fun A => A) := {|
-   ret := fun _ x => x;
-   bind := fun _ _ x k => k x;
-   ignore := fun _ x => ();
-   seq := fun _ x k => k;
-   map := fun _ _ f x => f x
- |}.
-
-End Id.
-
-Module IOBase.
-
- Parameter T : Set -> Set.
- Extract Constant T "'a" => "unit -> 'a".
- Parameter Ref : Set -> Set.
- Extract Constant Ref "'a" => "'a Pervasives.ref".
-
- Parameter ret : forall (A:Set), A -> T A.
- Extract Constant ret => "fun a -> (); fun () -> a".
- Extraction Implicit ret [A].
- Parameter bind : forall A B, T A -> (A->T B) -> T B.
- Extract Constant bind => "fun a k -> (); fun () -> k (a ()) ()".
- Extraction Implicit bind [A B].
- Parameter ignore : forall A, T A -> T unit.
- Extract Constant ignore => "fun a -> (); fun () -> ignore (a ())".
- Extraction Implicit ignore [A].
- Parameter seq : forall A, T unit -> T A -> T A.
- Extract Constant seq => "fun a k -> (); fun () -> a (); k ()".
- Extraction Implicit seq [A].
- Parameter map : forall (A B : Set), (A -> B) -> T A -> T B.
- Extract Constant map => "fun f a -> (); fun () -> f (a ())".
- Extraction Implicit map [A B].
-
- Parameter ref : forall (A:Set), A -> T (Ref A).
- Extract Constant ref => "fun a -> (); fun () -> Pervasives.ref a".
- Extraction Implicit ref [A].
- Parameter set : forall A, Ref A -> A -> T unit.
- Extract Constant set => "fun r a -> (); fun () -> Pervasives.(:=) r a".
- Extraction Implicit set [A].
- Parameter get : forall A, Ref A -> T A.
- Extract Constant get => "fun r -> (); fun () -> Pervasives.(!) r".
- Extraction Implicit get [A].
-
- Parameter raise : forall A, Exception -> T A.
- Extract Constant raise => "fun e -> (); fun () -> raise (Proof_errors.Exception e)".
- Extraction Implicit raise [A].
- Parameter catch : forall A, T A -> (Exception -> T A) -> T A.
- Extract Constant 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 ()".
- Extraction Implicit catch [A].
-
- Parameter read_line : T String.
- Extract Constant read_line => "fun () -> try Pervasives.read_line () with e -> let e = Errors.push e in raise e ()".
- Parameter print_char : Char -> T unit.
- Extract Constant print_char => "fun c -> (); fun () -> print_char c".
- Parameter print : Ppcmds -> T unit.
- Extract Constant print => "fun s -> (); fun () -> try Pp.pp s; Pp.pp_flush () with e -> let e = Errors.push e in raise e ()".
-
- Parameter timeout: forall A, Int -> T A -> T A.
- Extract Constant timeout => "fun n t -> (); fun () -> Control.timeout n t (Proof_errors.Exception Proof_errors.Timeout)".
- Extraction Implicit timeout [A].
-
-End IOBase.
-
-(* spiwack: IO is split in two modules to avoid moot dependencies and
-   useless extracted code. *)
-Module IO.
-
- Record S (Ref:Set->Set) (T:Set->Set) : Set := {
-   ref : forall {A:Set}, A -> T (Ref A);
-   set : forall {A:Set}, Ref A -> A -> T unit;
-   get : forall {A:Set}, Ref A -> T A;
-
-   read_line : T String;
-   print_char : Char -> T unit;
-   print : Ppcmds -> T unit;
-
-   raise : forall {A:Set}, Exception -> T A;
-   catch : forall {A:Set}, T A -> (Exception -> T A) -> T A;
-   timeout : forall {A:Set}, Int -> T A -> T A
- }.
-
- Definition T : Set -> Set := IOBase.T.
- Definition Ref : Set -> Set := IOBase.Ref.
-
- Definition M : Monad T := {|
-   ret := IOBase.ret;
-   bind := IOBase.bind;
-   ignore := IOBase.ignore;
-   seq := IOBase.seq;
-   map := IOBase.map
- |}.
-
- Definition IO : S Ref T := {|
-   ref := IOBase.ref;
-   set := IOBase.set;
-   get := IOBase.get;
-
-   read_line := IOBase.read_line;
-   print_char := IOBase.print_char;
-   print := IOBase.print;
-
-   raise := IOBase.raise;
-   catch := IOBase.catch;
-   timeout := IOBase.timeout
- |}.
-
-End IO.
-
-Module State.
-(** The impredicative encoding of the usual State monad transformer
-    (StateT in Haskell). The impredicative encoding allows to avoid
-    creating blocks (val,state) at each bind. *)
-
-Section Common.
-
- Variables (S:Set) (T₀:Set->Set) (M:Monad T₀).
-
- Definition T (A:Set):= forall R:Set, (A -> S -> T₀ R) -> S -> T₀ R.
-
- Definition F : Monad T := {|
-   ret A x := fun R k s => k x s ;
-   bind A B x f := fun R k s =>
-            x R (fun a s' => f a R k s') s ;
-   ignore A x := fun R k s =>
-            x R (fun _ s' => k tt s') s ;
-   seq A x y := fun R k s =>
-           x R (fun _ s' => y R k s') s;
-   map A B f x := fun R k s => x R (fun a s => k (f a) s) s
- |}.
-
- Definition State : State S T := {|
-   set s := (fun R k _ => k () s) : T unit  ;
-   get := fun R k s => k s s ;
-   modify := fun f R k s => k () (f s)
- |}.
-
- Definition lift {A} (x:T₀ A) : T A := fun R k s =>
-   do M x := x in
-   k x s
- .
-
- Definition run {A} (x:T A) (s:S) : T₀ (A*S) := x _ (fun a s' => ret _ M (a,s')) s.
- Definition reflect {A:Set} (x:S -> T₀ (A*S)) : T A := fun R k s =>
-   do M x' := x s in
-   let '(a,s') := x' in
-   k a s'
- .
-
-
- Variable (L:Logic T₀).
-
- Definition Logic : Logic T := {|
-   zero A e := lift (zero _ L e);
-   plus A x y := fun R k s => plus _ L (x R k s) (fun e => y e R k s)
- |}.
-
- Variable (Env:Set) (E:Environment Env T₀).
-
- Definition Environment : Environment Env T := {|
-   current := lift (current _ _ E)
- |}.
-
- Variable (C:Set) (W:Writer C T₀).
-
- Definition Writer : Writer C T := {|
-   put x := lift (put _ _ W x)
- |}.
-
-End Common.
-
-End State.
-
-
-Module Environment.
-(** The impredicative encoding of the usual environment monad
-    transformer (ReaderT in Haskell). The impredicative encoding
-    allows to avoid using the binding operations of the underlying
-    monad when it isn't explicitly needed. *)
-
-Section Common.
-
- Variable (E:Set) (T₀:Set->Set) (M:Monad T₀).
-
- Definition T (A:Set) := forall (R:Set), (A -> T₀ R)-> E-> T₀ R.
-
- Definition F : Monad T := {|
-   ret A x := fun R k e => k x;
-   bind A B x f := fun R k e => x _ (fun a => f a _ k e) e;
-   ignore A x := fun R k e => x _ (fun _ => k tt) e;
-   seq A x y := fun R k e => x _ (fun _ => y _ k e) e;
-   map A B f x := fun R k e => x _ (fun a => k (f a)) e
- |}.
-
- Definition Environment : Environment E T := {|
-   current := fun R k e => k e 
- |}.
-
-
- Definition lift {A:Set} (x:T₀ A) : T A := fun R k _ =>
-   do M x := x in
-   k x
- .
-
- Definition run {A:Set} (x:T A) (e:E) : T₀ A := x _ (fun a => ret _ M a) e.
- Definition reflect {A:Set} (m:E->T₀ A) : T A := fun R k e =>
-   do M m' := m e in
-   k m'
- .
-
-
- Variable (L:Logic T₀).
-
- Definition Logic : Logic T := {|
-   zero A e := lift (zero _ L e);
-   plus A x y := fun R k e => plus _ L (x _ k e) (fun exc => y exc _ k e)
- |}.
-
- Variable (C:Set) (W:Writer C T₀).
-
- Definition Writer : Writer C T := {|
-   put x := lift (put _ _ W x)
- |}.
-
-End Common.
-
-End Environment.
-
-Module Writer.
-(** The impredicative encoding of the usual "writer" monad
-    transformer (WriterT in Haskell). The impredicative encoding
-    allows to avoid using the binding operations of the underlying
-    monad when it isn't explicitly needed and to avoid constructing
-    and deconstructing values of the form (val,c). *)
-
-Section Common.
-
- Variables (C:Set) (m:Monoid.T C) (T₀:Set->Set) (M:Monad T₀).
-
- Definition T (A:Set) := forall (R:Set), (A->C->T₀ R) -> T₀ R.
-
- Definition F : Monad T := {|
-   ret A x := fun R k => k x (Monoid.zero _ m);
-   bind A B x f := fun R k =>
-     x _ (fun a c => f a _ (fun b c' => k b (Monoid.prod _ m c c')));
-   ignore A x := fun R k => x _ (fun _ c => k tt c);
-   seq A x y := fun R k =>
-     x _ (fun _ c => y _ (fun b c' => k b (Monoid.prod _ m c c')));
-   map A B f x := fun R k => x _ (fun a c => k (f a) c)
- |}.
-
- Definition Writer : Writer C T := {|
-   put c := ((fun R (k:unit->C->T₀ R) => k tt c):T unit)
- |}.
-
- Definition lift {A} (x:T₀ A) : T A := fun R k =>
-   do M x := x in
-   k x (Monoid.zero _ m)
- .
-
- Definition run {A} (x:T A) : T₀ (A*C)%type := x _ (fun a c => ret _ M (a,c)).
- Definition reflect {A:Set} (x:T₀ (A*C)) :T A := fun R k =>
-   do M x := x in
-   let '(a,c) := x in
-   k a c
- .
-
- Variable (L:Logic T₀).
-
- Definition Logic : Logic T := {|
-   zero A e := lift (zero _ L e);
-   plus A x y := fun R k => plus _ L (x _ k) (fun exc => y exc _ k)
- |}.
-
-End Common.
-
-End Writer.
-
-
-Module Logic.
-
-(* 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. Shan,
-   D. Friedman, and A. Sabry.  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. *)
-
-Section Common.
-
- Variables (T₀:Set->Set) (M:Monad T₀).
-
- Definition FK (R:Set) : Set := Exception -> R.
- Definition SK (A R:Set) : Set := A -> FK R -> R.
- Definition T (A:Set) : Set := forall (R:Set), SK A (T₀ R) -> FK (T₀ R) -> T₀ R.
- (* 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. *)
-
- Definition F : Monad T := {|
-   ret A x R sk fk := sk x fk;
-   bind A B x k R sk fk :=
-      x _ (fun a fk => k a _ sk fk) fk;
-   ignore A x R sk fk :=
-      x _ (fun _ fk => sk () fk) fk;
-   seq A x k R sk fk :=
-      x _ (fun _ fk => k _ sk fk) fk;
-   map A B f x R sk fk := x _ (fun a fk => sk (f a) fk) fk
- |}.
-
- Definition lift {A} (x:T₀ A) : T A := fun _ sk fk =>
-   do M x := x in
-   sk x fk
- .
-
- Definition _zero {A:Set} (e:Exception) : T A := fun _ _ fk => fk e.
- Definition _plus {A:Set} (x:T A) (y:Exception -> T A) : T A := fun _ sk fk =>
-   x _ sk (fun e => y e _ sk fk)
- .
-
- (* For [reflect] and [split] see the "Backtracking, Interleaving, and
-    Terminating Monad Transformers" paper.  *)
- Definition reflect {A:Set} (x:list_view A (Exception -> T A)) : T A :=
-   match x with
-   | Nil _ _ e => _zero e
-   | Cons _ _ a x => _plus (ret _ F a) x
-   end
- .
- Definition reify {A:Set} (x:T A) : T₀ (list_view A (Exception -> T A)) :=
-   let fk e := ret _ M (Nil _ _ e) in
-   let lift_fk fk e := do F y := lift (fk e) in reflect y in
-   let sk a fk := ret _ M (Cons _ _ a (lift_fk fk)) in
-   x _ sk fk
- .
-
- Definition split {A:Set} (x:T A) : T (list_view A (Exception -> T A)) :=
-   lift (reify x)
- .
-
- Definition Logic : Logic T := {|
-   zero := @_zero;
-   plus := @_plus
- |}.
-
- Variable (Ref:Set->Set) (IO:IO.S Ref T₀).
-
- Definition run {A:Set} (x:T A) : T₀ A :=
-   let sk (a:A) _ : T₀ A := ret _ M a in
-   let fk e : T₀ A := IO.raise _ _ IO (tactic_failure e) in
-   x _ sk fk
- .
-
-End Common.
-
-End Logic.
-
-
-(*** Extraction **)
-
-Parameters (constr types evar_map goal env seffs:Set).
-Extract Inlined Constant constr => "Term.constr".
-Extract Inlined Constant types => "Term.types".
-Extract Inlined Constant evar_map => "Evd.evar_map".
-Extract Inlined Constant goal => "Goal.goal".
-Extract Inlined Constant env => "Environ.env".
-
-Record proofview := {
-  solution : evar_map;
-  comb : list goal
-}.
-
-Definition LogicalState := proofview.
-(** Logical Message: status (safe/unsafe) * ( shelved goals * given up ) *)
-Definition LogicalMessageType := ( bool * ( list goal * list goal ))%type.
-Definition LogicalEnvironment := env.
-Definition LogicalMessage : Monoid.T LogicalMessageType :=
-  Monoid.cart Monoid.BoolAnd (Monoid.cart Monoid.List Monoid.List)
-.
-
-Definition NonLogicalType := IO.T.
-Definition NonLogicalMonad : Monad NonLogicalType := IO.M.
-Definition NonLogicalIO : IO.S IO.Ref NonLogicalType := IO.IO.
-
-Definition LogicType := Logic.T NonLogicalType.
-Definition WriterType := Writer.T LogicalMessageType LogicType.
-Definition EnvironmentType := Environment.T LogicalEnvironment WriterType.
-Definition LogicalType := State.T LogicalState EnvironmentType.
-Definition LogicalMonadBase := Logic.F NonLogicalType.
-Definition LogicalMonadWriter := Writer.F _ LogicalMessage LogicType.
-Definition LogicalMonadEnv := Environment.F LogicalEnvironment WriterType.
-Definition LogicalMonad : Monad LogicalType := State.F LogicalState _.
-Definition LogicalStateM : State LogicalState LogicalType := State.State LogicalState _.
-Definition LogicalReaderE : Environment LogicalEnvironment _ := Environment.Environment LogicalEnvironment WriterType.
-Definition LogicalReader : Environment LogicalEnvironment LogicalType := State.Environment _ _ LogicalMonadEnv _ LogicalReaderE.
-Definition LogicalWriterW : Writer LogicalMessageType  _ := Writer.Writer LogicalMessageType LogicType.
-Definition LogicalWriterE : Writer LogicalMessageType _ := Environment.Writer LogicalEnvironment _ LogicalMonadWriter LogicalMessageType LogicalWriterW.
-Definition LogicalWriter : Writer LogicalMessageType LogicalType := State.Writer _ _ LogicalMonadEnv _ LogicalWriterE.
-Definition LogicalLogic : Logic LogicalType := State.Logic _ _ LogicalMonadEnv (Environment.Logic _ _ LogicalMonadWriter (Writer.Logic _ LogicalMessage _ LogicalMonadBase (Logic.Logic _))).
-
-
-(* The function [split] will be define as the normal form of
-   [split0]. It reifies the monad transformer stack until we can read
-   back a more syntactic form, then reflects the result back. *)
-Definition split0 {a:Set} (x:LogicalType a) : LogicalType (list_view a (Exception -> LogicalType a)) :=
-  State.reflect _ _ LogicalMonadEnv (fun s =>
-  Environment.reflect _ _ LogicalMonadWriter (fun e =>
-  Writer.reflect _ _ LogicalMonadBase (
-    do LogicalMonadBase x' :=
-        Logic.split _ NonLogicalMonad (Writer.run _ _ LogicalMonadBase (Environment.run _ _ LogicalMonadWriter (State.run _ _ LogicalMonadEnv x s) e)) in
-    match x' with
-    | Nil _ _ exc => ret _ LogicalMonadBase ((Nil _ _ exc),s, Monoid.zero _ LogicalMessage)
-    | Cons _ _ (a',s',m') y =>
-      let y' exc :=
-          State.reflect _ _ LogicalMonadEnv (fun _ =>
-          Environment.reflect _ _ LogicalMonadWriter (fun _ =>
-          Writer.reflect _ _ LogicalMonadBase (y exc)))
-      in
-      ret _ LogicalMonadBase (Cons _ _ a' y',s',m')
-    end
-  )))
-.
-
-
-Module NonLogical.
-
- Definition t (a:Set) := Eval compute in NonLogicalType a.
- Definition ref (a:Set) := Eval compute in IO.Ref a.
-
- Definition ret {a:Set} (x:a) : t a := Eval compute in ret _ NonLogicalMonad x.
- Extraction Implicit ret [a].
- Definition bind {a b:Set} (x:t a) (k:a-> t b) : t b := Eval compute in bind _ NonLogicalMonad x k.
- Extraction Implicit bind [a b].
-
- Definition ignore {a:Set} (x:t a) : t unit := Eval compute in ignore _ NonLogicalMonad x.
- Extraction Implicit ignore [a].
- Definition seq {a:Set} (x:t unit) (k:t a) : t a := Eval compute in seq _ NonLogicalMonad x k.
- Extraction Implicit seq [a].
- Definition map {a b:Set} (f:a -> b) (x:t a) : t b := Eval compute in freeze _ (map _ NonLogicalMonad f x).
- Extraction Implicit map [a b].
-
- Definition new_ref {a:Set} (x:a) : t (ref a) := Eval compute in IO.ref _ _ NonLogicalIO x.
- Extraction Implicit new_ref [a].
- Definition set {a:Set} (r:ref a) (x:a) : t unit := Eval compute in IO.set _ _ NonLogicalIO r x.
- Extraction Implicit set [a].
- Definition get {a:Set} (r:ref a) : t a := Eval compute in IO.get _ _ NonLogicalIO r.
- Extraction Implicit get [a].
-
- Definition raise {a:Set} (e:Exception) : t a := Eval compute in IO.raise _ _ NonLogicalIO e.
- Extraction Implicit raise [a].
- Definition catch {a:Set} (s:t a) (h:Exception -> t a) : t a := Eval compute in IO.catch _ _ NonLogicalIO s h.
- Extraction Implicit catch [a].
- Definition timeout {a:Set} n (x:t a) : t a := Eval compute in IO.timeout _ _ NonLogicalIO n x.
- Extraction Implicit timeout [a].
-
- Definition read_line : t String := Eval compute in IO.read_line _ _ NonLogicalIO.
- Definition print_char (c:Char) : t unit := Eval compute in IO.print_char _ _ NonLogicalIO c.
- Definition print (s:Ppcmds) : t unit := Eval compute in IO.print _ _ NonLogicalIO s.
-
- (* /!\ The extracted code for [run] performs effects. /!\ *)
- Parameter run : forall a:Set, t a -> a.
- Extract Constant run => "fun x ->
-  try x () with Proof_errors.Exception e as src ->
-    let src = Errors.push src in
-    let e = Backtrace.app_backtrace ~src ~dst:e in
-    Pervasives.raise e".
- Extraction Implicit run [a].
-
-End NonLogical.
-
-Module Logical.
-
- Definition t (a:Set) := Eval compute in LogicalType a.
-
- Definition ret {a:Set} (x:a) : t a := Eval compute in freeze _ (ret _ LogicalMonad x).
- Extraction Implicit ret [a].
- Definition bind {a b:Set} (x:t a) (k:a-> t b) : t b := Eval compute in freeze _ (bind _ LogicalMonad x k).
- Extraction Implicit bind [a b].
- Definition ignore {a:Set} (x:t a) : t unit := Eval compute in freeze _ (ignore _ LogicalMonad x).
- Extraction Implicit ignore [a].
- Definition seq {a:Set} (x:t unit) (k:t a) : t a := Eval compute in freeze _ (seq _ LogicalMonad x k).
- Extraction Implicit seq [a].
- Definition map {a b:Set} (f:a -> b) (x:t a) : t b := Eval compute in freeze _ (map _ LogicalMonad f x).
- Extraction Implicit map [a b].
-
- Definition set (s:LogicalState) : t unit := Eval compute in freeze _ (set _ _ LogicalStateM s).
- Definition get : t LogicalState := Eval compute in get _ _ LogicalStateM.
- Definition modify (f : LogicalState -> LogicalState) : t unit := Eval compute in freeze _ (modify _ _ LogicalStateM f).
- Definition put (m:LogicalMessageType) : t unit := Eval compute in freeze _ (put _ _ LogicalWriter m).
- Definition current : t LogicalEnvironment := Eval compute in current _ _ LogicalReader.
-
- Definition zero {a:Set} (e:Exception) : t a := Eval compute in freeze _ (zero _ LogicalLogic e).
- Extraction Implicit zero [a].
- Definition plus {a:Set} (x:t a) (y:Exception -> t a) : t a := Eval compute in freeze _ (plus _ LogicalLogic x y).
- Extraction Implicit plus [a].
-
- Definition split {a:Set} (x:t a) : t (list_view a (Exception -> t a)) :=
-   Eval compute in freeze _ (split0 x).
- Extraction Implicit split [a].
- Definition lift {a:Set} (x:NonLogical.t a) : t a := Eval compute in
-  freeze _ (State.lift _ _ LogicalMonadEnv (Environment.lift _ _ LogicalMonadWriter (Writer.lift _ LogicalMessage _ LogicalMonadBase (Logic.lift _ NonLogicalMonad x)))).
- Extraction Implicit lift [a].
-
- Definition run {a:Set} (x:t a) (e:LogicalEnvironment) (s:LogicalState) : NonLogical.t ((a*LogicalState)*LogicalMessageType) := Eval compute in
-  Logic.run _ NonLogicalMonad _ NonLogicalIO (Writer.run _ _ LogicalMonadBase (Environment.run _ _ LogicalMonadWriter (State.run _ _ LogicalMonadEnv x s) e))
- .
- Extraction Implicit run [a].
-
-End Logical.
-
-Set Extraction Flag 1007.
-Set Extraction Conservative Types.
-Set Extraction File Comment "
-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.
-".
-
-Extraction "proofs/proofview_gen.ml" NonLogical Logical.
diff --git a/proofs/proof_errors.ml b/proofs/proof_errors.ml
deleted file mode 100644
index e543b0c8fd..0000000000
--- a/proofs/proof_errors.ml
+++ /dev/null
@@ -1,12 +0,0 @@
-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
deleted file mode 100644
index dd21d539c9..0000000000
--- a/proofs/proof_errors.mli
+++ /dev/null
@@ -1,18 +0,0 @@
-(** 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/proofview.ml b/proofs/proofview.ml
index 08a736278e..d207a03825 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -224,7 +224,7 @@ let apply env t sp =
 
 
 let catchable_exception = function
-  | Proof_errors.Exception _ -> false
+  | Proofview_monad.Exception _ -> false
   | e -> Errors.noncritical e
 
 
@@ -578,8 +578,8 @@ let tclTIMEOUT n t =
           (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 as src ->
+        | Proofview_monad.Timeout -> Proofview_monad.NonLogical.ret (Util.Inr Timeout)
+        | Proofview_monad.TacticFailure e as src ->
           let e = Backtrace.app_backtrace ~src ~dst:e in
           Proofview_monad.NonLogical.ret (Util.Inr e)
         | e -> Proofview_monad.NonLogical.raise e
@@ -812,7 +812,7 @@ module V82 = struct
       let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] } 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 as src ->
+    with Proofview_monad.TacticFailure e as src ->
       let src = Errors.push src in
       let e = Backtrace.app_backtrace ~src ~dst:e in
       raise e
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index b60673ac96..165f7a9b52 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -465,8 +465,8 @@ module NonLogical : sig
      [()]. *)
   val seq : unit t -> 'a t -> 'a t
 
-  (* [new_ref x] creates a reference containing [x]. *)
-  val new_ref : 'a -> 'a ref t
+  (* [ref x] creates a reference containing [x]. *)
+  val ref : 'a -> 'a ref t
   (* [set r x] assigns [x] to [r]. *)
   val set : 'a ref -> 'a -> unit t
   (* [get r] returns the value of [r] *)
diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml
index 90b730198b..d3e2b8df79 100644
--- a/proofs/proofview_gen.ml
+++ b/proofs/proofview_gen.ml
@@ -1,73 +1,155 @@
-type ('a, 'b) list_view =
-| Nil of exn
-| Cons of 'a * 'b
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** This file defines the low-level monadic operations used by the
+    tactic monad. The monad is divided into two layers: a non-logical
+    layer which consists in operations which will not (or cannot) be
+    backtracked in case of failure (input/output or persistent state)
+    and a logical layer which handles backtracking, proof
+    manipulation, and any other effect which needs to backtrack. *)
+
+(** {6 States of the logical monad} *)
+
+type proofview = { solution : Evd.evar_map; comb : Goal.goal list }
+
+(** Read/write *)
+type logicalState = proofview
 
-module IO =
- struct
+(** Write only. Must be a monoid.
+
+    Status (safe/unsafe) * ( shelved goals * given up ). *)
+type logicalMessageType = bool*(Goal.goal list*Goal.goal list)
+
+(** Read only *)
+type logicalEnvironment = Environ.env
+
+
+(** {6 Exceptions} *)
+
+
+(** 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
+
+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
+
+(** {6 Non-logical layer} *)
+
+(** The non-logical monad is a simple [unit -> 'a] (i/o) monad. The
+    operations are simple wrappers around corresponding usual
+    operations and require little documentation. *)
+module NonLogical =
+struct
   type 'a t = unit -> 'a
 
-  type 'a coq_Ref = 'a Pervasives.ref
+  type 'a ref = 'a Pervasives.ref
+
+  (* The functions in this module follow the pattern that they are
+     defined with the form [(); fun ()->...]. This is an optimisation
+     which signals to the compiler that the function is usually partially
+     applied up to the [();]. Without this annotation, partial
+     applications can be significantly slower.
+
+     Documentation of this behaviour can be found at:
+     https://ocaml.janestreet.com/?q=node/30 *)
 
-  let ret = fun a -> (); fun () -> a
+  let ret a = (); fun () -> a
 
-  let bind = fun a k -> (); fun () -> k (a ()) ()
+  let bind a k = (); fun () -> k (a ()) ()
 
-  let ignore = fun a -> (); fun () -> ignore (a ())
+  let ignore a = (); fun () -> ignore (a ())
 
-  let seq = fun a k -> (); fun () -> a (); k ()
+  let seq a k = (); fun () -> a (); k ()
 
-  let map = fun f a -> (); fun () -> f (a ())
+  let map f a = (); fun () -> f (a ())
 
-  let ref = fun a -> (); fun () -> Pervasives.ref a
+  let ref a = (); fun () -> Pervasives.ref a
 
-  let set = fun r a -> (); fun () -> Pervasives.(:=) r a
+  (** [Pervasives.(:=)] *)
+  let set r a = (); fun () -> r := a
 
-  let get = fun r -> (); fun () -> Pervasives.(!) r
+  (** [Pervasives.(!)] *)
+  let get = fun r -> (); fun () -> ! r
 
-  let raise = fun e -> (); fun () -> raise (Proof_errors.Exception e)
+  (** [Pervasives.raise]. Except that exceptions are wrapped with
+      {!Exception}. *)
+  let raise = fun e -> (); fun () -> raise (Exception e)
 
+  (** [try ... with ...] but restricted to {!Exception}. *)
   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 ()
+    fun () -> try s ()
+      with Exception e as src ->
+        let src = Errors.push src in
+        let e = Backtrace.app_backtrace ~src ~dst:e in
+        h e ()
 
   let read_line = fun () -> try Pervasives.read_line () with e -> let e = Errors.push e in raise e ()
 
   let print_char = fun c -> (); fun () -> print_char c
 
+  (** {!Pp.pp}. The buffer is also flushed. *)
   let print = fun s -> (); fun () -> try Pp.pp s; Pp.pp_flush () with e -> let e = Errors.push e in raise e ()
 
   let timeout = fun n t -> (); fun () ->
-    Control.timeout n t (Proof_errors.Exception Proof_errors.Timeout)
+    Control.timeout n t (Exception Timeout)
 
+  let run = fun x ->
+    try x () with Exception e as src ->
+      let src = Errors.push src in
+      let e = Backtrace.app_backtrace ~src ~dst:e in
+      Pervasives.raise e
 end
 
-type proofview = { solution : Evd.evar_map; comb : Goal.goal list }
+(** {6 Logical layer} *)
 
-type logicalState = proofview
+(** The logical monad is a backtracking monad on top of which is
+    layered a state monad (which is used to implement all of read/write,
+    read only, and write only effects). The state monad being layered on
+    top of the backtracking monad makes it so that the state is
+    backtracked on failure.
 
-type logicalMessageType = bool*(Goal.goal list*Goal.goal list)
+    Backtracking differs from regular exception in that, writing (+)
+    for exception catching and (>>=) for bind, we require the
+    following extra distributivity laws:
 
-type logicalEnvironment = Environ.env
+    x+(y+z) = (x+y)+z
 
-module NonLogical =
- struct
-  include IO
-  type 'a ref = 'a IO.coq_Ref
+    zero+x = x
 
-  let new_ref = ref
+    x+zero = x
 
-  let run = fun x ->
-  try x () with Proof_errors.Exception e as src ->
-    let src = Errors.push src in
-    let e = Backtrace.app_backtrace ~src ~dst:e in
-    Pervasives.raise e
- end
+    (x+y)>>=k = (x>>=k)+(y>>=k) *)
+
+(** A view type for the logical monad, which is a form of list, hence
+    we can decompose it with as a list. *)
+type ('a, 'b) list_view =
+  | Nil of exn
+  | Cons of 'a * 'b
 
 module Logical =
- struct
+struct
 
   type rt = logicalEnvironment
   type wt = logicalMessageType
@@ -83,8 +165,40 @@ module Logical =
 
   let merge (b1, (l1, k1)) (b2, (l2, k2)) = (b1 && b2, (l1 @ l2, k1 @ k2))
 
+  (** Double-continuation backtracking monads are reasonable folklore
+      for "search" implementations (including the 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. Shan, D. Friedman, and A. Sabry.  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.
+
+      A somewhat concrete view is that the type ['a iolist] is, in fact
+      the impredicative encoding of the following stream type:
+
+      [type 'a _iolist' = Nil of exn | Cons of 'a*'a iolist'
+       and 'a iolist = 'a _iolist NonLogical.t]
+
+      Using impredicative encoding avoids intermediate allocation and
+      is, empirically, very efficient in Ocaml. It also has the
+      practical benefit that the monadic operation are independent of
+      the underlying monad, which simplifies the code and side-steps
+      the limited inlining of Ocaml.
+
+      In that vision, [bind] is simply [concat_map] (though the cps
+      version is significantly simpler), [plus] is concatenation, and
+      [split] is pattern-matching. *)
   type 'a iolist =
-    { iolist : 'r. (exn -> 'r IO.t) -> ('a -> (exn -> 'r IO.t) -> 'r IO.t) -> 'r IO.t }
+      { iolist : 'r. (exn -> 'r NonLogical.t) ->
+                     ('a -> (exn -> 'r NonLogical.t) -> 'r NonLogical.t) ->
+                     'r NonLogical.t }
 
   type 'a tactic = state -> ('a * state) iolist
 
@@ -116,8 +230,8 @@ module Logical =
     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) }
+  let lift (m : 'a NonLogical.t) : 'a tactic = (); fun s ->
+    { iolist = fun nil cons -> NonLogical.bind m (fun x -> cons (x, s) nil) }
 
   (** State related *)
 
@@ -148,7 +262,9 @@ module Logical =
       m.iolist nil (fun x next -> cons x (fun e -> if f e then nil e else next e))
     }
 
-  type 'a reified = ('a, exn -> 'a reified) list_view IO.t
+  (** For [reflect] and [split] see the "Backtracking, Interleaving,
+      and Terminating Monad Transformers" paper.  *)
+  type 'a reified = ('a, exn -> 'a reified) list_view NonLogical.t
 
   let rec reflect (m : 'a reified) : 'a iolist =
     { iolist = fun nil cons ->
@@ -156,15 +272,15 @@ module Logical =
       | Nil e -> nil e
       | Cons (x, l) -> cons x (fun e -> (reflect (l e)).iolist nil cons)
       in
-      IO.bind m next
+      NonLogical.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
+    let rnil e = NonLogical.ret (Nil e) in
+    let rcons p l = NonLogical.ret (Cons (p, l)) in
     { iolist = fun nil cons ->
-      IO.bind (m.iolist rnil rcons) begin function
+      NonLogical.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
@@ -174,8 +290,8 @@ module Logical =
   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
+    let nil e = NonLogical.raise (TacticFailure e) in
+    let cons (x, s) _ = NonLogical.ret ((x, s.sstate), s.wstate) in
     m.iolist nil cons
 
  end
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli
index 6b6f216b0a..27aea3ae95 100644
--- a/proofs/proofview_monad.mli
+++ b/proofs/proofview_monad.mli
@@ -15,6 +15,25 @@ type logicalEnvironment = Environ.env
 type logicalMessageType = bool * ( Goal.goal list * Goal.goal list )
 
 
+(** {6 Exceptions} *)
+
+
+(** 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
+
 
 module NonLogical : sig
 
@@ -27,7 +46,7 @@ module NonLogical : sig
   val ignore : 'a t -> unit t
   val seq : unit t -> 'a t -> 'a t
 
-  val new_ref : 'a -> 'a ref t
+  val ref : 'a -> 'a ref t
   val set : 'a ref -> 'a -> unit t
   val get : 'a ref -> 'a t
 
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 1cc08fa49b..62b157307a 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -76,9 +76,9 @@ let goal_com tac =
 (* [run (new_ref _)] gives us a ref shared among [NonLogical.t]
    expressions. It avoids parametrizing everything over a
    reference. *)
-let skipped = Proofview.NonLogical.run (Proofview.NonLogical.new_ref 0)
-let skip = Proofview.NonLogical.run (Proofview.NonLogical.new_ref 0)
-let breakpoint = Proofview.NonLogical.run (Proofview.NonLogical.new_ref None)
+let skipped = Proofview.NonLogical.run (Proofview.NonLogical.ref 0)
+let skip = Proofview.NonLogical.run (Proofview.NonLogical.ref 0)
+let breakpoint = Proofview.NonLogical.run (Proofview.NonLogical.ref None)
 
 let rec drop_spaces inst i =
   if String.length inst > i && inst.[i] == ' ' then drop_spaces inst (i+1)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index cca26bf055..826846f906 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2120,7 +2120,7 @@ let _ =
       let prf = Proof.start sigma [env, ty] in
       let (prf, _) =
         try Proof.run_tactic env tac prf
-        with Proof_errors.TacticFailure e as src ->
+        with Proofview_monad.TacticFailure e as src ->
           (** Catch the inner error of the monad tactic *)
           let src = Errors.push src in
           let e = Backtrace.app_backtrace ~src ~dst:e in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 07ac0ba9f2..3b1cf65755 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3748,7 +3748,7 @@ let abstract_subproof id gk tac =
   let ectx = Evd.evar_universe_context evd in
   let (const, safe, ectx) =
     try Pfedit.build_constant_by_tactic ~goal_kind:gk id ectx secsign concl solve_tac
-    with Proof_errors.TacticFailure e as src ->
+    with Proofview_monad.TacticFailure e as src ->
     (* if the tactic [tac] fails, it reports a [TacticFailure e],
        which is an error irrelevant to the proof system (in fact it
        means that [e] comes from [tac] failing to yield enough
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 9c15b20686..4cf8f4145a 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -102,7 +102,7 @@ let process_vernac_interp_error exn = match exn with
       exc
 
 let rec strip_wrapping_exceptions = function
-  | Proof_errors.TacticFailure e as src ->
+  | Proofview_monad.TacticFailure e as src ->
     let e = Backtrace.app_backtrace ~src ~dst:e in
     strip_wrapping_exceptions e
   | exc -> exc