diff options
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 3 |
1 files changed, 3 insertions, 0 deletions
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 \ |