From ab46dacbe7d4a19b58ee319d63b50f1212cf7c49 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 21 Dec 2011 23:16:37 +0000
Subject: 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
---
 toplevel/toplevel.mllib | 1 -
 1 file changed, 1 deletion(-)

diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 4df717e102..8b03e93803 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -18,7 +18,6 @@ Mltop
 Vernacentries
 Whelp
 Vernac
-Interface
 Ide_intf
 Ide_slave
 Toplevel
-- 
cgit v1.2.3