diff options
| author |  vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-11 18:00:15 +0000 |
|---|---|---|
| committer | vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-11 18:00:15 +0000 |
| commit | 329d4502d6880483ad997cd53936cfaa21351ba2 (patch) | |
| tree | 5abda56ac92b41d72a5c486e8fa2f54ff0291bf8 /ide/ide.mllib | |
| parent | e61dee5744110f9316305aeaa4c363af7655a989 (diff) | |
Isolation of proof-displaying code
The formatting logic is now isolated in ide/proofBrowser.ml, and the
goal printing logic is deported inside ide/coq.ml. Also, the proof mode
special printing has been cut out. Finally, turn every call to
show_goals_full into show_goals, and use show_goals_full as the body of
show_goals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12648 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/ide.mllib')
| -rw-r--r-- | ide/ide.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/ide.mllib b/ide/ide.mllib index a235039b9..af620fd09 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -16,6 +16,7 @@ Ideutils CoqLex Gtk_parsing Undo +ProofBrowser Coq Coq_commands Coq_tactics |