diff options
| author | Maxime Dénès | 2018-03-09 10:24:18 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-09 10:24:18 +0100 |
| commit | fd852113ea205720a9394c27989acaac408f7643 (patch) | |
| tree | f3cb2d7b11c3bb161139ac81232c343c980c45e0 /engine/proofview.mli | |
| parent | 49dd2bddc03ce64707cb93d450127152ad6eece6 (diff) | |
| parent | e7bf157c6af0d7f65b0611f7dfa9c00d5e1e7a83 (diff) | |
Merge PR #6328: Fix #6313: lost goals in nested ltac in refine
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 |