Makefile: force the installation of all .cmi (and remove some obsolete .mli)

 The previous code wasn't detecting and installing .cmi coming from
 .mli without corresponding .ml.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14783 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 9 insertions, 38 deletions

diff --git a/Makefile.build b/Makefile.build
index a21bee1b36..0e49c13819 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -621,6 +621,14 @@ install-tools::
 	$(INSTALLLIB) tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc
 	$(INSTALLBIN) $(TOOLS) $(FULLBINDIR)
 
+# The list of .cmi to install, including the ones obtained
+# from .mli without .ml, and the ones obtained from .ml without .mli
+
+INSTALLCMI = $(sort \
+	$(CONFIG:.cmo=.cmi) \
+	$(filter-out checker/% ide/% tools/%, $(MLIFILES:.mli=.cmi)) \
+	$(foreach lib,$(CORECMA) $(PLUGINSCMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES)))))
+
 install-library:
 	$(MKDIR) $(FULLCOQLIB)
 	$(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS) $(PLUGINSOPT)
@@ -629,9 +637,7 @@ install-library:
 	$(MKDIR) $(FULLCOQLIB)/user-contrib
 	$(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)
 	$(INSTALLSH)  $(FULLCOQLIB) $(CONFIG) $(LINKCMO) $(GRAMMARCMA)
-	# reconstitute the list of core .cmi
-	$(INSTALLSH)  $(FULLCOQLIB) $(CONFIG:.cmo=.cmi) \
-	  $(foreach lib,$(CORECMA:.cma=_MLLIB_DEPENDENCIES) $(PLUGINSCMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .cmi,$($(lib))))
+	$(INSTALLSH)  $(FULLCOQLIB) $(INSTALLCMI)
 ifeq ($(BEST),opt)
 	$(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB)
 	$(INSTALLSH)  $(FULLCOQLIB) $(CONFIG:.cmo=.cmx) $(CONFIG:.cmo=.o) $(LINKCMO:.cma=.cmxa) $(LINKCMO:.cma=.a)
diff --git a/parsing/g_intsyntax.mli b/parsing/g_intsyntax.mli
deleted file mode 100644
index 7f7c88d352..0000000000
--- a/parsing/g_intsyntax.mli
+++ /dev/null
@@ -1,13 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-
-(*i $$ i*)
-
-
-(** digit based syntax for int31 and bigint *)
diff --git a/parsing/g_natsyntax.mli b/parsing/g_natsyntax.mli
deleted file mode 100644
index 3b137b866b..0000000000
--- a/parsing/g_natsyntax.mli
+++ /dev/null
@@ -1,13 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Nice syntax for naturals. *)
-
-open Notation
-
-val nat_of_int : Bigint.bigint prim_token_interpreter
diff --git a/parsing/g_zsyntax.mli b/parsing/g_zsyntax.mli
deleted file mode 100644
index 34e888bca1..0000000000
--- a/parsing/g_zsyntax.mli
+++ /dev/null
@@ -1,9 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Nice syntax for integers. *)