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?

0 files changed, 0 insertions, 0 deletions