aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--Makefile.build10
-rw-r--r--Makefile.common3
2 files changed, 4 insertions, 9 deletions
diff --git a/Makefile.build b/Makefile.build
index 3cea8b8a4..0a2186899 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -602,14 +602,6 @@ install-tools::
cp tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc
cp $(TOOLS) $(FULLBINDIR)
-GRAMMARCMA=parsing/grammar.cma
-OBJECTCMA=lib/lib.cma kernel/kernel.cma library/library.cma \
- pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
- parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \
- parsing/highparsing.cma tactics/hightactics.cma contrib/contrib.cma
-
-OBJECTCMXA=$(OBJECTCMA:.cma=.cmxa)
-
install-library:
$(MKDIR) $(FULLCOQLIB)
for f in $(LIBFILES); do \
@@ -619,7 +611,7 @@ install-library:
$(MKDIR) $(FULLCOQLIB)/states
cp states/*.coq $(FULLCOQLIB)/states
$(MKDIR) $(FULLCOQLIB)/user-contrib
- cp $(OBJECTCMA) $(OBJECTCMXA) $(GRAMMARCMA) $(FULLCOQLIB)
+ cp $(LINKCMO) $(LINKCMOCMXA) $(GRAMMARCMA) $(FULLCOQLIB)
install-library-light:
$(MKDIR) $(FULLCOQLIB)
diff --git a/Makefile.common b/Makefile.common
index 3cff1c762..004cef640 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -270,6 +270,7 @@ CMXA:=$(CMA:.cma=.cmxa)
# Beware that highparsing.cma should appear before hightactics.cma
# respecting this order is useful for developers that want to load or link
# the libraries directly
+
LINKCMO:=$(CONFIG) lib/lib.cma kernel/kernel.cma library/library.cma \
pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \
@@ -382,6 +383,8 @@ GRAMMARSCMO:=\
GRAMMARCMO:=$(GRAMMARNEEDEDCMO) $(CAMLP4EXTENSIONSCMO) $(GRAMMARSCMO)
+GRAMMARCMA:=parsing/grammar.cma
+
GRAMMARML4:=lib/compat.ml4 lib/pp.ml4 parsing/q_util.ml4 parsing/pcoq.ml4 \
parsing/argextend.ml4 parsing/tacextend.ml4 parsing/vernacextend.ml4 \
parsing/g_prim.ml4 parsing/g_tactic.ml4 \