diff options
| -rw-r--r-- | Makefile.build | 12 | ||||
| -rw-r--r-- | parsing/g_intsyntax.mli | 13 | ||||
| -rw-r--r-- | parsing/g_natsyntax.mli | 13 | ||||
| -rw-r--r-- | parsing/g_zsyntax.mli | 9 |
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. *) |