Make names in [Proofview_monad] more uniform.

ret -> return, bind -> (>>=), etc… So that monads expose a [Monad.S] signature. Also Proofview now exposes the [Monad.S] signature directly rather than in a [Monad.S] subdirectory.

1 files changed, 6 insertions, 13 deletions

diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli
index 675b4c768..c1315e9f5 100644
--- a/proofs/proofview_monad.mli
+++ b/proofs/proofview_monad.mli
@@ -41,20 +41,17 @@ exception TacticFailure of exn
     operations and require little documentation. *)
 module NonLogical : sig
 
-  type +'a t
-  type 'a ref
+  include Monad.S
 
-  val ret : 'a -> 'a t
-  val bind : 'a t -> ('a -> 'b t) -> 'b t
-  val map : ('a -> 'b) -> 'a t -> 'b t
   val ignore : 'a t -> unit t
-  val seq : unit t -> 'a t -> 'a t
+
+  type 'a ref
 
   val ref : 'a -> 'a ref t
   (** [Pervasives.(:=)] *)
-  val set : 'a ref -> 'a -> unit t
+  val (:=) : 'a ref -> 'a -> unit t
   (** [Pervasives.(!)] *)
-  val get : 'a ref -> 'a t
+  val (!) : 'a ref -> 'a t
 
   val read_line : string t
   val print_char : char -> unit t
@@ -125,13 +122,9 @@ end
 
 module Logical (P:Param) : sig
 
-  type +'a t
+  include Monad.S
 
-  val ret : 'a -> 'a t
-  val bind : 'a t -> ('a -> 'b t) -> 'b t
-  val map : ('a -> 'b) -> 'a t -> 'b t
   val ignore : 'a t -> unit t
-  val seq : unit t -> 'a t -> 'a t
 
   val set : P.s -> unit t
   val get : P.s t