diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-21 23:16:37 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-21 23:16:37 +0000 |
| commit | ab46dacbe7d4a19b58ee319d63b50f1212cf7c49 (patch) | |
| tree | 43dd27359eb6b536b85db0dcbb2363f6bcba67fe /toplevel/toplevel.mllib | |
| parent | fdbb03f1047fc2ba36895c8ed3ffbc79bc7314e2 (diff) | |
Pure interfaces shouldn't be mentionned in .mllib
.mllib should only mention *code* to be linked in .cma
and later executable, but not .mli without .ml.
Otherwise, really nasty errors occur with ocamlbuild,
for instance some rules appears to be ignored and masked
by default ones, etc etc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14840 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/toplevel.mllib')
| -rw-r--r-- | toplevel/toplevel.mllib | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index 4df717e10..8b03e9380 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -18,7 +18,6 @@ Mltop Vernacentries Whelp Vernac -Interface Ide_intf Ide_slave Toplevel |