aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proofview_monad.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proofview_monad.mli')
-rw-r--r--proofs/proofview_monad.mli2
1 files changed, 0 insertions, 2 deletions
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli
index c2a1ff52c..a459db424 100644
--- a/proofs/proofview_monad.mli
+++ b/proofs/proofview_monad.mli
@@ -134,8 +134,6 @@ module Logical : sig
val modify : (logicalState -> logicalState) -> unit t
val put : logicalMessageType -> unit t
val current : logicalEnvironment t
- val set_local : logicalEnvironment -> 'a t -> 'a t
- val modify_local : (logicalEnvironment->logicalEnvironment) -> 'a t -> 'a t
val zero : exn -> 'a t
val plus : 'a t -> (exn -> 'a t) -> 'a t