aboutsummaryrefslogtreecommitdiff
path: root/Makefile.dev
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.dev')
-rw-r--r--Makefile.dev24
1 files changed, 12 insertions, 12 deletions
diff --git a/Makefile.dev b/Makefile.dev
index b1e142333a..f48a6f0d8f 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -1,7 +1,7 @@
##########################################################################
## # The Coq Proof Assistant / The Coq Development Team ##
-## v # INRIA, CNRS and contributors - Copyright 1999-2019 ##
-## <O___,, # (see CREDITS file for the list of authors) ##
+## v # Copyright INRIA, CNRS and contributors ##
+## <O___,, # (see version control and CREDITS file for authors & dates) ##
## \VV/ ###############################################################
## // # This file is distributed under the terms of the ##
## # GNU Lesser General Public License Version 2.1 ##
@@ -140,17 +140,17 @@ noreal: unicode logic arith bool zarith qarith lists sets fsets \
### 4) plugins
################
-OMEGAVO:=$(filter plugins/omega/%, $(PLUGINSVO))
-MICROMEGAVO:=$(filter plugins/micromega/%, $(PLUGINSVO))
-RINGVO:=$(filter plugins/setoid_ring/%, $(PLUGINSVO))
-NSATZVO:=$(filter plugins/nsatz/%, $(PLUGINSVO))
-FUNINDVO:=$(filter plugins/funind/%, $(PLUGINSVO))
-BTAUTOVO:=$(filter plugins/btauto/%, $(PLUGINSVO))
-RTAUTOVO:=$(filter plugins/rtauto/%, $(PLUGINSVO))
-EXTRACTIONVO:=$(filter plugins/extraction/%, $(PLUGINSVO))
+OMEGAVO:=$(filter theories/omega/%, $(THEORIESVO))
+MICROMEGAVO:=$(filter theories/micromega/%, $(THEORIESVO))
+RINGVO:=$(filter theories/setoid_ring/%, $(THEORIESVO))
+NSATZVO:=$(filter theories/nsatz/%, $(THEORIESVO))
+FUNINDVO:=$(filter theories/funind/%, $(THEORIESVO))
+BTAUTOVO:=$(filter theories/btauto/%, $(THEORIESVO))
+RTAUTOVO:=$(filter theories/rtauto/%, $(THEORIESVO))
+EXTRACTIONVO:=$(filter theories/extraction/%, $(THEORIESVO))
CCVO:=
-DERIVEVO:=$(filter plugins/derive/%, $(PLUGINSVO))
-LTACVO:=$(filter plugins/ltac/%, $(PLUGINSVO))
+DERIVEVO:=$(filter theories/derive/%, $(THEORIESVO))
+LTACVO:=$(filter theories/ltac/%, $(THEORIESVO))
omega: $(OMEGAVO) $(OMEGACMO)
micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT)