diff options
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common index 17dd694d8..6fe218863 100644 --- a/Makefile.common +++ b/Makefile.common @@ -616,7 +616,8 @@ FSETSBASEVO:=\ FSETS_basic:= FSETS_all:=\ - theories/FSets/FMapAVL.vo theories/FSets/FSetAVL.vo \ + theories/FSets/FSetAVL.vo theories/FSets/FSetFullAVL.vo \ + theories/FSets/FMapAVL.vo FSETSVO:=$(FSETSBASEVO) $(FSETS_$(FSETS)) |