aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-09-30 09:54:35 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-09-30 09:54:35 +0200
commit504018731249475d1ab57a97e7cbd3842b13e984 (patch)
tree74e0d1b6dc9be57ccc5d503ebda032e9f15579a6 /Makefile.common
parenta478947e33bcca34291ec36487876443a694c6bf (diff)
Build the compatibility files.
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common4
1 files changed, 3 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common
index 8f3d39bf2..92a48cd6c 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -302,6 +302,7 @@ SETOIDSVO:=$(call cat_vo_itarget, theories/Setoids)
UNICODEVO:=$(call cat_vo_itarget, theories/Unicode)
CLASSESVO:=$(call cat_vo_itarget, theories/Classes)
PROGRAMVO:=$(call cat_vo_itarget, theories/Program)
+COMPATVO:=$(call cat_vo_itarget, theories/Compat)
THEORIESVO:=\
$(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) \
@@ -311,7 +312,8 @@ THEORIESVO:=\
$(PARITHVO) $(NARITHVO) $(ZARITHVO) \
$(SETSVO) $(FSETSVO) $(MSETSVO) $(MMAPSVO) \
$(REALSVO) $(SORTINGVO) $(QARITHVO) \
- $(NUMBERSVO) $(STRUCTURESVO) $(VECTORSVO)
+ $(NUMBERSVO) $(STRUCTURESVO) $(VECTORSVO) \
+ $(COMPATVO)
THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(UNICODEVO) $(ARITHVO)