diff options
Diffstat (limited to 'proofs/proofview_monad.ml')
-rw-r--r-- | proofs/proofview_monad.ml | 25 |
1 files changed, 15 insertions, 10 deletions
diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml index 6e68cd2e..e9bc7761 100644 --- a/proofs/proofview_monad.ml +++ b/proofs/proofview_monad.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -157,8 +157,11 @@ 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 } - +type proofview = { + solution : Evd.evar_map; + comb : Goal.goal list; + shelf : Goal.goal list; +} (** {6 Instantiation of the logic monad} *) @@ -171,10 +174,10 @@ module P = struct type e = bool (** Status (safe/unsafe) * shelved goals * given up *) - type w = bool * Evar.t list * Evar.t list + type w = bool * Evar.t list - let wunit = true , [] , [] - let wprod (b1,s1,g1) (b2,s2,g2) = b1 && b2 , s1@s2 , g1@g2 + let wunit = true , [] + let wprod (b1, g1) (b2, g2) = b1 && b2 , g1@g2 type u = Info.state @@ -226,19 +229,21 @@ module Env : State with type t := Environ.env = struct end module Status : Writer with type t := bool = struct - let put s = Logical.put (s,[],[]) + let put s = Logical.put (s, []) end -module Shelf : Writer with type t = Evar.t list = struct +module Shelf : 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 put sh = Logical.put (true,sh,[]) + let get = Logical.map (fun {shelf} -> shelf) Pv.get + let set c = Pv.modify (fun pv -> { pv with shelf = c }) + let modify f = Pv.modify (fun pv -> { pv with shelf = f pv.shelf }) 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) + let put gs = Logical.put (true, gs) end (** Lens and utilies pertaining to the info trace *) |