diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-01-13 18:38:38 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-01-13 18:38:38 +0000 |
| commit | 28000ead7870114795b21b3cc819aadc4dab329d (patch) | |
| tree | d711c345dbb911cea4ecef1d0721a9aa6da7c3cd /Makefile.common | |
| parent | 04b99a94d308eec12ecc7b0143122fe34d86ee90 (diff) | |
Added a Btauto plugin, that solves boolean tautologies.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14897 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/Makefile.common b/Makefile.common index b560bae5a..d4492736a 100644 --- a/Makefile.common +++ b/Makefile.common @@ -82,7 +82,7 @@ SRCDIRS:=\ omega romega micromega quote ring dp \ setoid_ring xml extraction fourier \ cc funind firstorder field subtac \ - rtauto nsatz syntax decl_mode) + rtauto nsatz syntax decl_mode btauto) # Order is relevent here because kernel and checker contain files # with the same name @@ -185,6 +185,7 @@ FUNINDCMA:=plugins/funind/recdef_plugin.cma FOCMA:=plugins/firstorder/ground_plugin.cma CCCMA:=plugins/cc/cc_plugin.cma SUBTACCMA:=plugins/subtac/subtac_plugin.cma +BTAUTOCMA:=plugins/btauto/btauto_plugin.cma RTAUTOCMA:=plugins/rtauto/rtauto_plugin.cma NATSYNTAXCMA:=plugins/syntax/nat_syntax_plugin.cma OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \ @@ -198,7 +199,7 @@ DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cma PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \ $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(DPCMA) $(FIELDCMA) \ $(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \ - $(CCCMA) $(FOCMA) $(SUBTACCMA) $(RTAUTOCMA) \ + $(CCCMA) $(FOCMA) $(SUBTACCMA) $(RTAUTOCMA) $(BTAUTOCMA) \ $(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA) ifneq ($(HASNATDYNLINK),false) @@ -315,6 +316,7 @@ NSATZVO:=$(call cat_vo_itarget, plugins/nsatz) FOURIERVO:=$(call cat_vo_itarget, plugins/fourier) FUNINDVO:=$(call cat_vo_itarget, plugins/funind) DPVO:=$(call cat_vo_itarget, plugins/dp) +BTAUTOVO:=$(call cat_vo_itarget, plugins/btauto) RTAUTOVO:=$(call cat_vo_itarget, plugins/rtauto) EXTRACTIONVO:=$(call cat_vo_itarget, plugins/extraction) XMLVO:= @@ -322,7 +324,7 @@ CCVO:= PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \ $(XMLVO) $(FOURIERVO) $(CCVO) $(FUNINDVO) \ - $(RTAUTOVO) $(NEWRINGVO) $(DPVO) $(QUOTEVO) \ + $(RTAUTOVO) $(BTAUTOVO) $(NEWRINGVO) $(DPVO) $(QUOTEVO) \ $(NSATZVO) $(EXTRACTIONVO) ALLVO:= $(THEORIESVO) $(PLUGINSVO) |