aboutsummaryrefslogtreecommitdiff
path: root/Makefile.common
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common9
1 files changed, 7 insertions, 2 deletions
diff --git a/Makefile.common b/Makefile.common
index bd0e19cd00..ee3bfb43c5 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -104,10 +104,14 @@ PLUGINDIRS:=\
rtauto nsatz syntax btauto \
ssrmatching ltac ssr
+USERCONTRIBDIRS:=\
+ Ltac2
+
SRCDIRS:=\
$(CORESRCDIRS) \
tools tools/coqdoc \
- $(addprefix plugins/, $(PLUGINDIRS))
+ $(addprefix plugins/, $(PLUGINDIRS)) \
+ $(addprefix user-contrib/, $(USERCONTRIBDIRS))
COQRUN := coqrun
LIBCOQRUN:=kernel/byterun/lib$(COQRUN).a
@@ -149,13 +153,14 @@ DERIVECMO:=plugins/derive/derive_plugin.cmo
LTACCMO:=plugins/ltac/ltac_plugin.cmo plugins/ltac/tauto_plugin.cmo
SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo
SSRCMO:=plugins/ssr/ssreflect_plugin.cmo
+LTAC2CMO:=user-contrib/Ltac2/ltac2_plugin.cmo
PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(MICROMEGACMO) \
$(RINGCMO) \
$(EXTRACTIONCMO) \
$(CCCMO) $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \
$(FUNINDCMO) $(NSATZCMO) $(SYNTAXCMO) \
- $(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO)
+ $(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO) $(LTAC2CMO)
ifeq ($(HASNATDYNLINK)-$(BEST),false-opt)
STATICPLUGINS:=$(PLUGINSCMO)