From b731022c022cfeae9203f6b10b4e1f68b85d9071 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 17 Feb 2018 22:59:32 +0100 Subject: 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? --- engine/proofview.ml | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'engine/proofview.ml') 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 }) -- cgit v1.2.3