diff options
| author | Arnaud Spiwack | 2013-11-25 19:55:57 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2013-12-04 14:14:32 +0100 |
| commit | eef907ed0a200e912ab2eddc0fcea41b5f61c145 (patch) | |
| tree | 9748713b4502fb7a5a020b834fee3d37f15644d2 /plugins/xml/xmlcommand.ml | |
| 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 'plugins/xml/xmlcommand.ml')
0 files changed, 0 insertions, 0 deletions