diff options
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 486279187..e7be66552 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 |