diff options
| author |  vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-12 17:50:33 +0000 |
|---|---|---|
| committer | vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-12 17:50:33 +0000 |
| commit | ae0aa7b06204025bf22223823ab07e640e6cf094 (patch) | |
| tree | dd9a85fd4525d9fa11fe67aae616677010564aba /library/lib.ml | |
| parent | 088e63c756bafd5224016a079e9a1f43191a242c (diff) | |
Delineating a API for Coq inside toplevel/vernac.ml
Coq use case are mostly thoses :
- parsing a char stream to get a vernac expr
- evaluating a vernac expr with backtracking
- turning a knob with a vernac expr, no backtracking
- loading an entire file
- compiling an entire file
- backtracking (no clean API for this yet)
- peeking Coq state info (no clean API for this yet)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12756 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/lib.ml')
0 files changed, 0 insertions, 0 deletions