diff options
| author | Pierre-Marie Pédrot | 2014-09-04 12:12:03 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-04 12:57:33 +0200 |
| commit | fc7a66d58c39e3d57e509c754fb4cefa96ecd488 (patch) | |
| tree | 43c6a5d626b4ba182723998d31ffbe99c38d114a /proofs/proofview_monad.mli | |
| parent | 6b0c471723a657048e50c94ea56387d54ef6eff6 (diff) | |
Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."
This reverts commit 664b3cba1e8d326382ca981aa49fdf00edd429e6.
Conflicts:
proofs/proofview.ml
Diffstat (limited to 'proofs/proofview_monad.mli')
| -rw-r--r-- | proofs/proofview_monad.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli index c2a1ff52c3..a459db424d 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 |