From ed9d3351cbcfae19db963903493f7669394a1fd3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 28 Feb 2015 01:06:30 +0100
Subject: Moving Proofview_monad to the engine/ folder.

---
 engine/engine.mllib        |   1 +
 engine/proofview_monad.ml  | 270 +++++++++++++++++++++++++++++++++++++++++++++
 engine/proofview_monad.mli | 144 ++++++++++++++++++++++++
 proofs/proofs.mllib        |   1 -
 proofs/proofview_monad.ml  | 270 ---------------------------------------------
 proofs/proofview_monad.mli | 144 ------------------------
 6 files changed, 415 insertions(+), 415 deletions(-)
 create mode 100644 engine/proofview_monad.ml
 create mode 100644 engine/proofview_monad.mli
 delete mode 100644 proofs/proofview_monad.ml
 delete mode 100644 proofs/proofview_monad.mli

diff --git a/engine/engine.mllib b/engine/engine.mllib
index 4073f7e44d..dc7ff2a642 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -2,3 +2,4 @@ Logic_monad
 Termops
 Namegen
 Evd
+Proofview_monad
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
new file mode 100644
index 0000000000..6e68cd2e45
--- /dev/null
+++ b/engine/proofview_monad.ml
@@ -0,0 +1,270 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** This file defines the datatypes used as internal states by the
+    tactic monad, and specialises the [Logic_monad] to these type. *)
+
+(** {6 Trees/forest for traces} *)
+
+module Trace = struct
+
+  (** The intent is that an ['a forest] is a list of messages of type
+      ['a]. But messages can stand for a list of more precise
+      messages, hence the structure is organised as a tree. *)
+  type 'a forest = 'a tree list
+  and  'a tree   = Seq of 'a * 'a forest
+
+  (** To build a trace incrementally, we use an intermediary data
+      structure on which we can define an S-expression like language
+      (like a simplified xml except the closing tags do not carry a
+      name). Note that nodes are built from right to left in ['a
+      incr], the result is mirrored when returning so that in the
+      exposed interface, the forest is read from left to right.
+
+      Concretely, we want to add a new tree to a forest: and we are
+      building it by adding new trees to the left of its left-most
+      subtrees which is built the same way. *)
+  type 'a incr = { head:'a forest ; opened: 'a tree list }
+
+  (** S-expression like language as ['a incr] transformers. It is the
+      responsibility of the library builder not to use [close] when no
+      tag is open. *)
+  let empty_incr = { head=[] ; opened=[] }
+  let opn a { head ; opened } = { head ; opened = Seq(a,[])::opened }
+  let close { head ; opened } =
+    match opened with
+    | [a] -> { head = a::head ; opened=[] }
+    | a::Seq(b,f)::opened -> { head ; opened=Seq(b,a::f)::opened }
+    | [] -> assert false
+  let leaf a s = close (opn a s)
+
+  (** Returning a forest. It is the responsibility of the library
+      builder to close all the tags. *)
+  (* spiwack: I may want to close the tags instead, to deal with
+     interruptions. *)
+  let rec mirror f = List.rev_map mirror_tree f
+  and mirror_tree (Seq(a,f)) = Seq(a,mirror f)
+
+  let to_tree = function
+    | { head ; opened=[] } -> mirror head
+    | { head ; opened=_::_} -> assert false
+
+end
+
+
+
+(** {6 State types} *)
+
+(** We typically label nodes of [Trace.tree] with messages to
+    print. But we don't want to compute the result. *)
+type lazy_msg = unit -> Pp.std_ppcmds
+let pr_lazy_msg msg = msg ()
+
+(** Info trace. *)
+module Info = struct
+
+  (** The type of the tags for [info]. *)
+  type tag =
+    | Msg of lazy_msg (** A simple message *)
+    | Tactic of lazy_msg (** A tactic call *)
+    | Dispatch  (** A call to [tclDISPATCH]/[tclEXTEND] *)
+    | DBranch  (** A special marker to delimit individual branch of a dispatch. *)
+
+  type state = tag Trace.incr
+  type tree = tag Trace.forest
+
+
+
+  let pr_in_comments m = Pp.(str"(* "++pr_lazy_msg m++str" *)")
+
+  let unbranch = function
+    | Trace.Seq (DBranch,brs) -> brs
+    | _ -> assert false
+
+
+  let is_empty_branch = let open Trace in function
+    | Seq(DBranch,[]) -> true
+    | _ -> false
+
+  (** Dispatch with empty branches are (supposed to be) equivalent to
+      [idtac] which need not appear, so they are removed from the
+      trace. *)
+  let dispatch brs =
+    let open Trace in
+    if CList.for_all is_empty_branch brs then None
+    else Some (Seq(Dispatch,brs))
+
+  let constr = let open Trace in function
+    | Dispatch -> dispatch
+    | t -> fun br -> Some (Seq(t,br))
+
+  let rec compress_tree = let open Trace in function
+    | Seq(t,f) -> constr t (compress f)
+  and compress f =
+    CList.map_filter compress_tree f
+
+  let rec is_empty = let open Trace in function
+    | Seq(Dispatch,brs) -> List.for_all is_empty brs
+    | Seq(DBranch,br) -> List.for_all is_empty br
+    | _ -> false
+
+  (** [with_sep] is [true] when [Tactic m] must be printed with a
+      trailing semi-colon. *)
+  let rec pr_tree with_sep = let open Trace in function
+    | Seq (Msg m,[]) -> pr_in_comments m
+    | Seq (Tactic m,_) ->
+        let tail = if with_sep then Pp.str";" else Pp.mt () in
+        Pp.(pr_lazy_msg m ++ tail)
+    | Seq (Dispatch,brs) ->
+        let tail = if with_sep then Pp.str";" else Pp.mt () in
+        Pp.(pr_dispatch brs++tail)
+    | Seq (Msg _,_::_) | Seq (DBranch,_) -> assert false
+  and pr_dispatch brs =
+    let open Pp in
+    let brs = List.map unbranch brs in
+    match brs with
+    | [br] -> pr_forest br
+    | _ ->
+        let sep () = spc()++str"|"++spc() in
+        let branches = prlist_with_sep sep pr_forest brs in
+        str"[>"++spc()++branches++spc()++str"]"
+  and pr_forest = function
+    | [] -> Pp.mt ()
+    | [tr] -> pr_tree false tr
+    | tr::l -> Pp.(pr_tree true tr ++ pr_forest l)
+
+  let print f =
+    pr_forest (compress f)
+
+  let rec collapse_tree n t =
+    let open Trace in
+    match n , t with
+    | 0 , t -> [t]
+    | _ , (Seq(Tactic _,[]) as t) -> [t]
+    | n , Seq(Tactic _,f) -> collapse (pred n) f
+    | n , Seq(Dispatch,brs) -> [Seq(Dispatch, (collapse n brs))]
+    | n , Seq(DBranch,br) -> [Seq(DBranch, (collapse n br))]
+    | _ , (Seq(Msg _,_) as t) -> [t]
+  and collapse n f =
+    CList.map_append (collapse_tree n) f
+end
+
+
+(** Type of proof views: current [evar_map] together with the list of
+    focused goals. *)
+type proofview = { solution : Evd.evar_map; comb : Goal.goal list }
+
+
+(** {6 Instantiation of the logic monad} *)
+
+(** Parameters of the logic monads *)
+module P = struct
+
+  type s = proofview * Environ.env
+
+  (** Recording info trace (true) or not. *)
+  type e = bool
+
+  (** Status (safe/unsafe) * shelved goals * given up *)
+  type w = bool * Evar.t list * Evar.t list
+
+  let wunit = true , [] , []
+  let wprod (b1,s1,g1) (b2,s2,g2) = b1 && b2 , s1@s2 , g1@g2
+
+  type u = Info.state
+
+  let uunit = Trace.empty_incr
+
+end
+
+module Logical = Logic_monad.Logical(P)
+
+
+(** {6 Lenses to access to components of the states} *)
+
+module type State = sig
+  type t
+  val get : t Logical.t
+  val set : t -> unit Logical.t
+  val modify : (t->t) -> unit Logical.t
+end
+
+module type Writer = sig
+  type t
+  val put : t -> unit Logical.t
+end
+
+module Pv : State with type t := proofview = struct
+  let get = Logical.(map fst get)
+  let set p = Logical.modify (fun (_,e) -> (p,e))
+  let modify f= Logical.modify (fun (p,e) -> (f p,e))
+end
+
+module Solution : State with type t := Evd.evar_map = struct
+  let get = Logical.map (fun {solution} -> solution) Pv.get
+  let set s = Pv.modify (fun pv -> { pv with solution = s })
+  let modify f = Pv.modify (fun pv -> { pv with solution = f pv.solution })
+end
+
+module Comb : State with type t = Evar.t list = struct
+    (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
+  type t = Evar.t list
+  let get = Logical.map (fun {comb} -> comb) Pv.get
+  let set c = Pv.modify (fun pv -> { pv with comb = c })
+  let modify f = Pv.modify (fun pv -> { pv with comb = f pv.comb })
+end
+
+module Env : State with type t := Environ.env = struct
+  let get = Logical.(map snd get)
+  let set e = Logical.modify (fun (p,_) -> (p,e))
+  let modify f = Logical.modify (fun (p,e) -> (p,f e))
+end
+
+module Status : Writer with type t := bool = struct
+  let put s = Logical.put (s,[],[])
+end
+
+module Shelf : Writer with type t = Evar.t list = struct
+    (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
+  type t = Evar.t list
+  let put sh = Logical.put (true,sh,[])
+end
+
+module Giveup : Writer with type t = Evar.t list = struct
+    (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
+  type t = Evar.t list
+  let put gs = Logical.put (true,[],gs)
+end
+
+(** Lens and utilies pertaining to the info trace *)
+module InfoL = struct
+  let recording = Logical.current
+  let if_recording t =
+    let open Logical in
+    recording >>= fun r ->
+    if r then t else return ()
+
+  let record_trace t = Logical.local true t
+
+  let raw_update = Logical.update
+  let update f = if_recording (raw_update f)
+  let opn a = update (Trace.opn a)
+  let close = update Trace.close
+  let leaf a = update (Trace.leaf a)
+
+  let tag a t =
+    let open Logical in
+    recording >>= fun r ->
+    if r then begin
+      raw_update (Trace.opn a) >>
+      t >>= fun a ->
+      raw_update Trace.close >>
+      return a
+    end else
+      t
+end
diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
new file mode 100644
index 0000000000..d2a2e55fb1
--- /dev/null
+++ b/engine/proofview_monad.mli
@@ -0,0 +1,144 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** This file defines the datatypes used as internal states by the
+    tactic monad, and specialises the [Logic_monad] to these type. *)
+
+(** {6 Traces} *)
+
+module Trace : sig
+
+  (** The intent is that an ['a forest] is a list of messages of type
+      ['a]. But messages can stand for a list of more precise
+      messages, hence the structure is organised as a tree. *)
+  type 'a forest = 'a tree list
+  and  'a tree   = Seq of 'a * 'a forest
+
+  (** To build a trace incrementally, we use an intermediary data
+      structure on which we can define an S-expression like language
+      (like a simplified xml except the closing tags do not carry a
+      name). *)
+  type 'a incr
+  val to_tree : 'a incr -> 'a forest
+
+  (** [open a] opens a tag with name [a]. *)
+  val opn : 'a -> 'a incr -> 'a incr
+
+  (** [close] closes the last open tag. It is the responsibility of
+      the user to close all the tags. *)
+  val close : 'a incr -> 'a incr
+
+  (** [leaf] creates an empty tag with name [a]. *)
+  val leaf : 'a -> 'a incr -> 'a incr
+
+end
+
+(** {6 State types} *)
+
+(** We typically label nodes of [Trace.tree] with messages to
+    print. But we don't want to compute the result. *)
+type lazy_msg = unit -> Pp.std_ppcmds
+
+(** Info trace. *)
+module Info : sig
+
+  (** The type of the tags for [info]. *)
+  type tag =
+    | Msg of lazy_msg (** A simple message *)
+    | Tactic of lazy_msg (** A tactic call *)
+    | Dispatch  (** A call to [tclDISPATCH]/[tclEXTEND] *)
+    | DBranch  (** A special marker to delimit individual branch of a dispatch. *)
+
+  type state = tag Trace.incr
+  type tree = tag Trace.forest
+
+  val print : tree -> Pp.std_ppcmds
+
+  (** [collapse n t] flattens the first [n] levels of [Tactic] in an
+      info trace, effectively forgetting about the [n] top level of
+      names (if there are fewer, the last name is kept). *)
+  val collapse : int -> tree -> tree
+
+end
+
+(** Type of proof views: current [evar_map] together with the list of
+    focused goals. *)
+type proofview = { solution : Evd.evar_map; comb : Goal.goal list }
+
+(** {6 Instantiation of the logic monad} *)
+
+module P : sig
+  type s = proofview * Environ.env
+
+  (** Status (safe/unsafe) * shelved goals * given up *)
+  type w = bool * Evar.t list * Evar.t list
+
+  val wunit : w
+  val wprod : w -> w -> w
+
+  (** Recording info trace (true) or not. *)
+  type e = bool
+
+  type u = Info.state
+
+  val uunit : u
+end
+
+module Logical : module type of Logic_monad.Logical(P)
+
+
+(** {6 Lenses to access to components of the states} *)
+
+module type State = sig
+  type t
+  val get : t Logical.t
+  val set : t -> unit Logical.t
+  val modify : (t->t) -> unit Logical.t
+end
+
+module type Writer = sig
+  type t
+  val put : t -> unit Logical.t
+end
+
+(** Lens to the [proofview]. *)
+module Pv : State with type t := proofview
+
+(** Lens to the [evar_map] of the proofview. *)
+module Solution : State with type t := Evd.evar_map
+
+(** Lens to the list of focused goals. *)
+module Comb : State with type t = Evar.t list
+
+(** Lens to the global environment. *)
+module Env : State with type t := Environ.env
+
+(** Lens to the tactic status ([true] if safe, [false] if unsafe) *)
+module Status : Writer with type t := bool
+
+(** Lens to the list of goals which have been shelved during the
+    execution of the tactic. *)
+module Shelf : Writer with type t = Evar.t list
+
+(** Lens to the list of goals which were given up during the execution
+    of the tactic. *)
+module Giveup : Writer with type t = Evar.t list
+
+(** Lens and utilies pertaining to the info trace *)
+module InfoL : sig
+  (** [record_trace t] behaves like [t] and compute its [info] trace. *)
+  val record_trace : 'a Logical.t -> 'a Logical.t
+
+  val update : (Info.state -> Info.state) -> unit Logical.t
+  val opn : Info.tag -> unit Logical.t
+  val close : unit Logical.t
+  val leaf : Info.tag -> unit Logical.t
+
+  (** [tag a t] opens tag [a] runs [t] then closes the tag. *)
+  val tag : Info.tag -> 'a Logical.t -> 'a Logical.t
+end
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index de08791272..1bd701cb9b 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -4,7 +4,6 @@ Evar_refiner
 Proof_using
 Proof_type
 Proof_errors
-Proofview_monad
 Logic
 Proofview
 Proof
diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml
deleted file mode 100644
index 6e68cd2e45..0000000000
--- a/proofs/proofview_monad.ml
+++ /dev/null
@@ -1,270 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** This file defines the datatypes used as internal states by the
-    tactic monad, and specialises the [Logic_monad] to these type. *)
-
-(** {6 Trees/forest for traces} *)
-
-module Trace = struct
-
-  (** The intent is that an ['a forest] is a list of messages of type
-      ['a]. But messages can stand for a list of more precise
-      messages, hence the structure is organised as a tree. *)
-  type 'a forest = 'a tree list
-  and  'a tree   = Seq of 'a * 'a forest
-
-  (** To build a trace incrementally, we use an intermediary data
-      structure on which we can define an S-expression like language
-      (like a simplified xml except the closing tags do not carry a
-      name). Note that nodes are built from right to left in ['a
-      incr], the result is mirrored when returning so that in the
-      exposed interface, the forest is read from left to right.
-
-      Concretely, we want to add a new tree to a forest: and we are
-      building it by adding new trees to the left of its left-most
-      subtrees which is built the same way. *)
-  type 'a incr = { head:'a forest ; opened: 'a tree list }
-
-  (** S-expression like language as ['a incr] transformers. It is the
-      responsibility of the library builder not to use [close] when no
-      tag is open. *)
-  let empty_incr = { head=[] ; opened=[] }
-  let opn a { head ; opened } = { head ; opened = Seq(a,[])::opened }
-  let close { head ; opened } =
-    match opened with
-    | [a] -> { head = a::head ; opened=[] }
-    | a::Seq(b,f)::opened -> { head ; opened=Seq(b,a::f)::opened }
-    | [] -> assert false
-  let leaf a s = close (opn a s)
-
-  (** Returning a forest. It is the responsibility of the library
-      builder to close all the tags. *)
-  (* spiwack: I may want to close the tags instead, to deal with
-     interruptions. *)
-  let rec mirror f = List.rev_map mirror_tree f
-  and mirror_tree (Seq(a,f)) = Seq(a,mirror f)
-
-  let to_tree = function
-    | { head ; opened=[] } -> mirror head
-    | { head ; opened=_::_} -> assert false
-
-end
-
-
-
-(** {6 State types} *)
-
-(** We typically label nodes of [Trace.tree] with messages to
-    print. But we don't want to compute the result. *)
-type lazy_msg = unit -> Pp.std_ppcmds
-let pr_lazy_msg msg = msg ()
-
-(** Info trace. *)
-module Info = struct
-
-  (** The type of the tags for [info]. *)
-  type tag =
-    | Msg of lazy_msg (** A simple message *)
-    | Tactic of lazy_msg (** A tactic call *)
-    | Dispatch  (** A call to [tclDISPATCH]/[tclEXTEND] *)
-    | DBranch  (** A special marker to delimit individual branch of a dispatch. *)
-
-  type state = tag Trace.incr
-  type tree = tag Trace.forest
-
-
-
-  let pr_in_comments m = Pp.(str"(* "++pr_lazy_msg m++str" *)")
-
-  let unbranch = function
-    | Trace.Seq (DBranch,brs) -> brs
-    | _ -> assert false
-
-
-  let is_empty_branch = let open Trace in function
-    | Seq(DBranch,[]) -> true
-    | _ -> false
-
-  (** Dispatch with empty branches are (supposed to be) equivalent to
-      [idtac] which need not appear, so they are removed from the
-      trace. *)
-  let dispatch brs =
-    let open Trace in
-    if CList.for_all is_empty_branch brs then None
-    else Some (Seq(Dispatch,brs))
-
-  let constr = let open Trace in function
-    | Dispatch -> dispatch
-    | t -> fun br -> Some (Seq(t,br))
-
-  let rec compress_tree = let open Trace in function
-    | Seq(t,f) -> constr t (compress f)
-  and compress f =
-    CList.map_filter compress_tree f
-
-  let rec is_empty = let open Trace in function
-    | Seq(Dispatch,brs) -> List.for_all is_empty brs
-    | Seq(DBranch,br) -> List.for_all is_empty br
-    | _ -> false
-
-  (** [with_sep] is [true] when [Tactic m] must be printed with a
-      trailing semi-colon. *)
-  let rec pr_tree with_sep = let open Trace in function
-    | Seq (Msg m,[]) -> pr_in_comments m
-    | Seq (Tactic m,_) ->
-        let tail = if with_sep then Pp.str";" else Pp.mt () in
-        Pp.(pr_lazy_msg m ++ tail)
-    | Seq (Dispatch,brs) ->
-        let tail = if with_sep then Pp.str";" else Pp.mt () in
-        Pp.(pr_dispatch brs++tail)
-    | Seq (Msg _,_::_) | Seq (DBranch,_) -> assert false
-  and pr_dispatch brs =
-    let open Pp in
-    let brs = List.map unbranch brs in
-    match brs with
-    | [br] -> pr_forest br
-    | _ ->
-        let sep () = spc()++str"|"++spc() in
-        let branches = prlist_with_sep sep pr_forest brs in
-        str"[>"++spc()++branches++spc()++str"]"
-  and pr_forest = function
-    | [] -> Pp.mt ()
-    | [tr] -> pr_tree false tr
-    | tr::l -> Pp.(pr_tree true tr ++ pr_forest l)
-
-  let print f =
-    pr_forest (compress f)
-
-  let rec collapse_tree n t =
-    let open Trace in
-    match n , t with
-    | 0 , t -> [t]
-    | _ , (Seq(Tactic _,[]) as t) -> [t]
-    | n , Seq(Tactic _,f) -> collapse (pred n) f
-    | n , Seq(Dispatch,brs) -> [Seq(Dispatch, (collapse n brs))]
-    | n , Seq(DBranch,br) -> [Seq(DBranch, (collapse n br))]
-    | _ , (Seq(Msg _,_) as t) -> [t]
-  and collapse n f =
-    CList.map_append (collapse_tree n) f
-end
-
-
-(** Type of proof views: current [evar_map] together with the list of
-    focused goals. *)
-type proofview = { solution : Evd.evar_map; comb : Goal.goal list }
-
-
-(** {6 Instantiation of the logic monad} *)
-
-(** Parameters of the logic monads *)
-module P = struct
-
-  type s = proofview * Environ.env
-
-  (** Recording info trace (true) or not. *)
-  type e = bool
-
-  (** Status (safe/unsafe) * shelved goals * given up *)
-  type w = bool * Evar.t list * Evar.t list
-
-  let wunit = true , [] , []
-  let wprod (b1,s1,g1) (b2,s2,g2) = b1 && b2 , s1@s2 , g1@g2
-
-  type u = Info.state
-
-  let uunit = Trace.empty_incr
-
-end
-
-module Logical = Logic_monad.Logical(P)
-
-
-(** {6 Lenses to access to components of the states} *)
-
-module type State = sig
-  type t
-  val get : t Logical.t
-  val set : t -> unit Logical.t
-  val modify : (t->t) -> unit Logical.t
-end
-
-module type Writer = sig
-  type t
-  val put : t -> unit Logical.t
-end
-
-module Pv : State with type t := proofview = struct
-  let get = Logical.(map fst get)
-  let set p = Logical.modify (fun (_,e) -> (p,e))
-  let modify f= Logical.modify (fun (p,e) -> (f p,e))
-end
-
-module Solution : State with type t := Evd.evar_map = struct
-  let get = Logical.map (fun {solution} -> solution) Pv.get
-  let set s = Pv.modify (fun pv -> { pv with solution = s })
-  let modify f = Pv.modify (fun pv -> { pv with solution = f pv.solution })
-end
-
-module Comb : State with type t = Evar.t list = struct
-    (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
-  type t = Evar.t list
-  let get = Logical.map (fun {comb} -> comb) Pv.get
-  let set c = Pv.modify (fun pv -> { pv with comb = c })
-  let modify f = Pv.modify (fun pv -> { pv with comb = f pv.comb })
-end
-
-module Env : State with type t := Environ.env = struct
-  let get = Logical.(map snd get)
-  let set e = Logical.modify (fun (p,_) -> (p,e))
-  let modify f = Logical.modify (fun (p,e) -> (p,f e))
-end
-
-module Status : Writer with type t := bool = struct
-  let put s = Logical.put (s,[],[])
-end
-
-module Shelf : Writer with type t = Evar.t list = struct
-    (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
-  type t = Evar.t list
-  let put sh = Logical.put (true,sh,[])
-end
-
-module Giveup : Writer with type t = Evar.t list = struct
-    (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
-  type t = Evar.t list
-  let put gs = Logical.put (true,[],gs)
-end
-
-(** Lens and utilies pertaining to the info trace *)
-module InfoL = struct
-  let recording = Logical.current
-  let if_recording t =
-    let open Logical in
-    recording >>= fun r ->
-    if r then t else return ()
-
-  let record_trace t = Logical.local true t
-
-  let raw_update = Logical.update
-  let update f = if_recording (raw_update f)
-  let opn a = update (Trace.opn a)
-  let close = update Trace.close
-  let leaf a = update (Trace.leaf a)
-
-  let tag a t =
-    let open Logical in
-    recording >>= fun r ->
-    if r then begin
-      raw_update (Trace.opn a) >>
-      t >>= fun a ->
-      raw_update Trace.close >>
-      return a
-    end else
-      t
-end
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli
deleted file mode 100644
index d2a2e55fb1..0000000000
--- a/proofs/proofview_monad.mli
+++ /dev/null
@@ -1,144 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** This file defines the datatypes used as internal states by the
-    tactic monad, and specialises the [Logic_monad] to these type. *)
-
-(** {6 Traces} *)
-
-module Trace : sig
-
-  (** The intent is that an ['a forest] is a list of messages of type
-      ['a]. But messages can stand for a list of more precise
-      messages, hence the structure is organised as a tree. *)
-  type 'a forest = 'a tree list
-  and  'a tree   = Seq of 'a * 'a forest
-
-  (** To build a trace incrementally, we use an intermediary data
-      structure on which we can define an S-expression like language
-      (like a simplified xml except the closing tags do not carry a
-      name). *)
-  type 'a incr
-  val to_tree : 'a incr -> 'a forest
-
-  (** [open a] opens a tag with name [a]. *)
-  val opn : 'a -> 'a incr -> 'a incr
-
-  (** [close] closes the last open tag. It is the responsibility of
-      the user to close all the tags. *)
-  val close : 'a incr -> 'a incr
-
-  (** [leaf] creates an empty tag with name [a]. *)
-  val leaf : 'a -> 'a incr -> 'a incr
-
-end
-
-(** {6 State types} *)
-
-(** We typically label nodes of [Trace.tree] with messages to
-    print. But we don't want to compute the result. *)
-type lazy_msg = unit -> Pp.std_ppcmds
-
-(** Info trace. *)
-module Info : sig
-
-  (** The type of the tags for [info]. *)
-  type tag =
-    | Msg of lazy_msg (** A simple message *)
-    | Tactic of lazy_msg (** A tactic call *)
-    | Dispatch  (** A call to [tclDISPATCH]/[tclEXTEND] *)
-    | DBranch  (** A special marker to delimit individual branch of a dispatch. *)
-
-  type state = tag Trace.incr
-  type tree = tag Trace.forest
-
-  val print : tree -> Pp.std_ppcmds
-
-  (** [collapse n t] flattens the first [n] levels of [Tactic] in an
-      info trace, effectively forgetting about the [n] top level of
-      names (if there are fewer, the last name is kept). *)
-  val collapse : int -> tree -> tree
-
-end
-
-(** Type of proof views: current [evar_map] together with the list of
-    focused goals. *)
-type proofview = { solution : Evd.evar_map; comb : Goal.goal list }
-
-(** {6 Instantiation of the logic monad} *)
-
-module P : sig
-  type s = proofview * Environ.env
-
-  (** Status (safe/unsafe) * shelved goals * given up *)
-  type w = bool * Evar.t list * Evar.t list
-
-  val wunit : w
-  val wprod : w -> w -> w
-
-  (** Recording info trace (true) or not. *)
-  type e = bool
-
-  type u = Info.state
-
-  val uunit : u
-end
-
-module Logical : module type of Logic_monad.Logical(P)
-
-
-(** {6 Lenses to access to components of the states} *)
-
-module type State = sig
-  type t
-  val get : t Logical.t
-  val set : t -> unit Logical.t
-  val modify : (t->t) -> unit Logical.t
-end
-
-module type Writer = sig
-  type t
-  val put : t -> unit Logical.t
-end
-
-(** Lens to the [proofview]. *)
-module Pv : State with type t := proofview
-
-(** Lens to the [evar_map] of the proofview. *)
-module Solution : State with type t := Evd.evar_map
-
-(** Lens to the list of focused goals. *)
-module Comb : State with type t = Evar.t list
-
-(** Lens to the global environment. *)
-module Env : State with type t := Environ.env
-
-(** Lens to the tactic status ([true] if safe, [false] if unsafe) *)
-module Status : Writer with type t := bool
-
-(** Lens to the list of goals which have been shelved during the
-    execution of the tactic. *)
-module Shelf : Writer with type t = Evar.t list
-
-(** Lens to the list of goals which were given up during the execution
-    of the tactic. *)
-module Giveup : Writer with type t = Evar.t list
-
-(** Lens and utilies pertaining to the info trace *)
-module InfoL : sig
-  (** [record_trace t] behaves like [t] and compute its [info] trace. *)
-  val record_trace : 'a Logical.t -> 'a Logical.t
-
-  val update : (Info.state -> Info.state) -> unit Logical.t
-  val opn : Info.tag -> unit Logical.t
-  val close : unit Logical.t
-  val leaf : Info.tag -> unit Logical.t
-
-  (** [tag a t] opens tag [a] runs [t] then closes the tag. *)
-  val tag : Info.tag -> 'a Logical.t -> 'a Logical.t
-end
-- 
cgit v1.2.3