diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2013-11-25 19:55:57 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2013-12-04 14:14:32 +0100 |
| commit | eef907ed0a200e912ab2eddc0fcea41b5f61c145 (patch) | |
| tree | 9748713b4502fb7a5a020b834fee3d37f15644d2 /proofs/proofview.mli | |
| parent | 12a55370b525185858aed77af4ef1dc0d5cf4e7e (diff) | |
Allow proofs to start with dependent goals.
I use a telescope to represent to goals, and let proofview.ml generate the appropriate existential variables.
Diffstat (limited to 'proofs/proofview.mli')
| -rw-r--r-- | proofs/proofview.mli | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli index b9251fffb..2f215ba94 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -38,6 +38,15 @@ val proofview : proofview -> Goal.goal list * Evd.evar_map conclusion types, creating that many initial goals. *) val init : Evd.evar_map -> (Environ.env * Term.types) list -> proofview +type telescope = + | TNil + | TCons of Environ.env*Term.types*(Term.constr -> telescope) + +(* Like [init], but goals are allowed to be depedenent on one + another. Dependencies between goals is represented with the type + [telescope] instead of [list]. *) +val dependent_init : Evd.evar_map -> telescope -> proofview + (* Returns whether this proofview is finished or not. That is, if it has empty subgoals in the comb. There could still be unsolved subgoaled, but they would then be out of the view, focused out. *) |