diff options
| author | Hugo Herbelin | 2018-02-17 22:59:32 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-08 21:58:31 +0100 |
| commit | b731022c022cfeae9203f6b10b4e1f68b85d9071 (patch) | |
| tree | 582bb7c6d3a05c194514c6a5ee9397dee849a8a3 /engine/proofview.mli | |
| parent | 61c9bd4bc14d3479a98c2b53adf1b86fa84f13bf (diff) | |
Adding tclPUTGIVENUP/tclPUTSHELF in Proofview.Unsafe.
Adding also tclSETSHELF/tclGETSHELF by consistency with
tclSETGOALS/tclGETGOALS.
However, I feel that this is too low-level to be exported as a
"tcl". Doesn't a "tcl" mean that it is supposed to be used by common
tactics? But is it reasonable that a common tactic can change and
modify comb and shelf without passing by a level which e.g. checks
that no goal is lost in the process.
So, I would rather be in favor of removing tclSETGOALS/tclGETGOALS
which are anyway aliases for Comb.get/Comb.set.
Conversely, what is the right expected level of abstraction for
proofview.ml?
Diffstat (limited to 'engine/proofview.mli')
| -rw-r--r-- | engine/proofview.mli | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/engine/proofview.mli b/engine/proofview.mli index 4862791874..e7be665527 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -435,6 +435,18 @@ module Unsafe : sig (** [tclGETGOALS] returns the list of goals under focus. *) val tclGETGOALS : Proofview_monad.goal_with_state list tactic + (** [tclSETSHELF gls] sets goals [gls] as the current shelf. *) + val tclSETSHELF : Evar.t list -> unit tactic + + (** [tclGETSHELF] returns the list of goals on the shelf. *) + val tclGETSHELF : Evar.t list tactic + + (** [tclPUTSHELF] appends goals to the shelf. *) + val tclPUTSHELF : Evar.t list -> unit tactic + + (** [tclPUTGIVENUP] add an given up goal. *) + val tclPUTGIVENUP : Evar.t list -> unit tactic + (** Sets the evar universe context. *) val tclEVARUNIVCONTEXT : UState.t -> unit tactic |