diff options
| author | Maxime Dénès | 2018-03-04 16:30:15 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-04 16:30:15 +0100 |
| commit | 346e73cef9e4e89c90f9f6f7011d54e3a0a35d96 (patch) | |
| tree | 07ccc997e8e13eac81d2c2a7dc5d63284dfbdf77 /engine/proofview.mli | |
| parent | ed05111e048e864c63c2e21b8ebac675a80dc464 (diff) | |
| parent | a131ebf7b66e31dea7d8ccfb9706ad6d8f4a12e0 (diff) | |
Merge PR #6676: [proofview] goals come with a state
Diffstat (limited to 'engine/proofview.mli')
| -rw-r--r-- | engine/proofview.mli | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/engine/proofview.mli b/engine/proofview.mli index 721ce507d4..77f30746d8 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -72,7 +72,15 @@ val return : proofview -> Evd.evar_map val partial_proof : entry -> proofview -> constr list val initial_goals : entry -> (constr * types) list +(** goal <-> goal_with_state *) +val with_empty_state : + Proofview_monad.goal -> Proofview_monad.goal_with_state +val drop_state : + Proofview_monad.goal_with_state -> Proofview_monad.goal +val goal_with_state : + Proofview_monad.goal -> Proofview_monad.StateStore.t -> + Proofview_monad.goal_with_state (** {6 Focusing commands} *) @@ -416,14 +424,14 @@ module Unsafe : sig (** [tclNEWGOALS gls] adds the goals [gls] to the ones currently being proved, appending them to the list of focused goals. If a goal is already solved, it is not added. *) - val tclNEWGOALS : Evar.t list -> unit tactic + val tclNEWGOALS : Proofview_monad.goal_with_state list -> unit tactic (** [tclSETGOALS gls] sets goals [gls] as the goals being under focus. If a goal is already solved, it is not set. *) - val tclSETGOALS : Evar.t list -> unit tactic + val tclSETGOALS : Proofview_monad.goal_with_state list -> unit tactic (** [tclGETGOALS] returns the list of goals under focus. *) - val tclGETGOALS : Evar.t list tactic + val tclGETGOALS : Proofview_monad.goal_with_state list tactic (** Sets the evar universe context. *) val tclEVARUNIVCONTEXT : UState.t -> unit tactic @@ -480,6 +488,7 @@ module Goal : sig val env : t -> Environ.env val sigma : t -> Evd.evar_map val extra : t -> Evd.Store.t + val state : t -> Proofview_monad.StateStore.t (** [nf_enter t] applies the goal-dependent tactic [t] in each goal independently, in the manner of {!tclINDEPENDENT} except that |