aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-21 14:50:25 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-06 17:41:37 +0200
commit014749917e5de9fe1885a1b1edc52b01cefa6f3f (patch)
tree5b6952c2d67b1c18ce5f6e22cc75cefc005ad460 /Makefile.common
parent0a577d3c979af094ca00be3e7e323109c7e1f6ab (diff)
Merge the ssr plugin.
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common5
1 files changed, 3 insertions, 2 deletions
diff --git a/Makefile.common b/Makefile.common
index b936eb4c7..4545fad05 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -62,7 +62,7 @@ PLUGINDIRS:=\
setoid_ring extraction fourier \
cc funind firstorder derive \
rtauto nsatz syntax btauto \
- ssrmatching ltac
+ ssrmatching ltac ssr
SRCDIRS:=\
$(CORESRCDIRS) \
@@ -120,13 +120,14 @@ OTHERSYNTAXCMO:=$(addprefix plugins/syntax/, \
DERIVECMO:=plugins/derive/derive_plugin.cmo
LTACCMO:=plugins/ltac/ltac_plugin.cmo
SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo
+SSRCMO:=plugins/ssr/ssreflect_plugin.cmo
PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \
$(QUOTECMO) $(RINGCMO) \
$(FOURIERCMO) $(EXTRACTIONCMO) \
$(CCCMO) $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \
$(FUNINDCMO) $(NSATZCMO) $(NATSYNTAXCMO) $(OTHERSYNTAXCMO) \
- $(DERIVECMO) $(SSRMATCHINGCMO)
+ $(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO)
ifeq ($(HASNATDYNLINK)-$(BEST),false-opt)
STATICPLUGINS:=$(PLUGINSCMO)