diff options
| author | Hugo Herbelin | 2014-10-12 15:32:38 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-13 19:12:34 +0200 |
| commit | 267d7a63e9c24573226d0890bedb783f10dcb235 (patch) | |
| tree | 9086f77abd7a96d89d9b9e9272ac4aa87f256223 /proofs/proofview.mli | |
| parent | 9632987e1eb0b035c760ab293e785c752d5eac92 (diff) | |
Adding a tactic which fails if one of the goals under focus is dependent in another one.
Diffstat (limited to 'proofs/proofview.mli')
| -rw-r--r-- | proofs/proofview.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli index e2d331c67c..671bd414ea 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -267,6 +267,10 @@ val shelve : unit tactic considered). *) val shelve_unifiable : unit tactic +(* This fails with error UnresolvedBindings if some goals are + dependent in the current list of goals under focus *) +val check_no_dependencies : unit tactic + (* [unshelve l p] adds all the goals in [l] at the end of the focused goals of p *) val unshelve : Goal.goal list -> proofview -> proofview |