diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-23 17:18:57 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-23 17:18:57 +0000 |
| commit | e84e0f9e4eb6263e870deb1e00929170bc0301ea (patch) | |
| tree | 7a792a8f40c5328c0bd385cec13cb4a65a6b8a3d /toplevel/toplevel.mllib | |
| parent | 461798eeecfd2a59159fb9666874d8ea14209624 (diff) | |
Ide: stronger separation from coqtop
Former module Ide_blob is now divided in Ide_intf (linked both
by coqtop and coqide) and Ide_slave (now only in coqtop).
Ide_intf has almost no dependencies, we can now compile coqide
with only coq_config.cm* and lib.cm(x)a
TODO:
- Devise a better way to display whether coqide is byte or opt
in the about message (instead of Mltop.is_native, I display
now the executable name, which hopefully contains opt or byte)
- Check the late error handling in ide/coq.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13927 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/toplevel.mllib')
| -rw-r--r-- | toplevel/toplevel.mllib | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index 7443edefd..8b03e9380 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -18,7 +18,8 @@ Mltop Vernacentries Whelp Vernac -Ide_blob +Ide_intf +Ide_slave Toplevel Usage Coqinit |