diff options
| author | Pierre-Marie Pédrot | 2014-05-24 14:40:50 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-05-24 15:10:17 +0200 |
| commit | b0364eff4ec8ad5676060d8ca9cdbbb1d9c34d04 (patch) | |
| tree | 5edfafa33d312bd827246271dd014cf56b3d4514 /proofs/proofview.mli | |
| parent | 6252e413a81cb45a6b1f5f24b25ab1c5ab8d0de6 (diff) | |
Chasing the goal entering backward while interpreting tactics. This required
writing a new primitive recovering the first goal under focus. It sounds a bit
hackish, but it does actually work.
Diffstat (limited to 'proofs/proofview.mli')
| -rw-r--r-- | proofs/proofview.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 6177803c78..769bfb001f 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -453,3 +453,6 @@ end (* [tclLIFT c] includes the non-logical command [c] in a tactic. *) val tclLIFT : 'a NonLogical.t -> 'a tactic + +(* Access the current goals *) +val tclGOALS : [ `NF ] Goal.t list tactic |