diff options
| author | msozeau | 2012-03-14 09:53:06 +0000 |
|---|---|---|
| committer | msozeau | 2012-03-14 09:53:06 +0000 |
| commit | 8ff2de8c01b3ba3563517627b1f5c9eb2c4bcb77 (patch) | |
| tree | 4f7e99ba36af1cf03d8c3315c371293ae46fe77c /Makefile.common | |
| parent | 4d7b12f27a7cc520a319a9d4b652137c0a0cbb60 (diff) | |
Final part of moving Program code inside the main code. Adapted add_definition/fixpoint and parsing of the "Program" prefix.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15036 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/Makefile.common b/Makefile.common index 88f035ac47..5f32ee13fc 100644 --- a/Makefile.common +++ b/Makefile.common @@ -81,7 +81,7 @@ SRCDIRS:=\ $(addprefix plugins/, \ omega romega micromega quote ring dp \ setoid_ring xml extraction fourier \ - cc funind firstorder field subtac \ + cc funind firstorder field \ rtauto nsatz syntax decl_mode btauto) # Order is relevent here because kernel and checker contain files @@ -184,7 +184,6 @@ EXTRACTIONCMA:=plugins/extraction/extraction_plugin.cma 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 @@ -199,13 +198,13 @@ 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) $(BTAUTOCMA) \ + $(CCCMA) $(FOCMA) $(RTAUTOCMA) $(BTAUTOCMA) \ $(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA) ifneq ($(HASNATDYNLINK),false) STATICPLUGINS:= INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) $(DPCMA) \ - $(XMLCMA) $(FUNINDCMA) $(SUBTACCMA) $(NATSYNTAXCMA) + $(XMLCMA) $(FUNINDCMA) $(NATSYNTAXCMA) INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs) PLUGINS:=$(PLUGINSCMA) PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs) |