aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-02-17 22:59:32 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-08 21:58:31 +0100
commitb731022c022cfeae9203f6b10b4e1f68b85d9071 (patch)
tree582bb7c6d3a05c194514c6a5ee9397dee849a8a3
parent61c9bd4bc14d3479a98c2b53adf1b86fa84f13bf (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?
-rw-r--r--engine/proofview.ml9
-rw-r--r--engine/proofview.mli12
2 files changed, 21 insertions, 0 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 73f26c320..53b3cdd9b 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1010,6 +1010,15 @@ module Unsafe = struct
let tclSETGOALS = Comb.set
+ let tclGETSHELF = Shelf.get
+
+ let tclSETSHELF = Shelf.set
+
+ let tclPUTSHELF to_shelve =
+ tclBIND tclGETSHELF (fun shelf -> tclSETSHELF (to_shelve@shelf))
+
+ let tclPUTGIVENUP = Giveup.put
+
let tclEVARSADVANCE evd =
Pv.modify (fun ps -> { ps with solution = evd; comb = undefined evd ps.comb })
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