diff options
Diffstat (limited to 'engine/proofview_monad.mli')
| -rw-r--r-- | engine/proofview_monad.mli | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli index af866528c8..6cca3f5a5e 100644 --- a/engine/proofview_monad.mli +++ b/engine/proofview_monad.mli @@ -83,7 +83,6 @@ val map_goal_with_state : (goal -> goal) -> goal_with_state -> goal_with_state type proofview = { solution : Evd.evar_map; comb : goal_with_state list; - shelf : goal list; } (** {6 Instantiation of the logic monad} *) @@ -137,10 +136,6 @@ 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 : State with type t = goal list - (** Lens and utilities pertaining to the info trace *) module InfoL : sig (** [record_trace t] behaves like [t] and compute its [info] trace. *) |