aboutsummaryrefslogtreecommitdiff
path: root/Makefile.common
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common6
1 files changed, 3 insertions, 3 deletions
diff --git a/Makefile.common b/Makefile.common
index cd0d6ab790..1325eabcf1 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -751,9 +751,9 @@ CCVO:=
DPVO:=contrib/dp/Dp.vo
-SUBTACVO:=contrib/subtac/SubtacTactics.vo contrib/subtac/Heq.vo \
- contrib/subtac/Utils.vo contrib/subtac/FixSub.vo contrib/subtac/Subtac.vo \
- contrib/subtac/FunctionalExtensionality.vo
+SUBTACVO:=theories/Program/Tactics.vo theories/Program/Heq.vo \
+ theories/Program/Utils.vo theories/Program/FixSub.vo theories/Program/Program.vo \
+ theories/Program/FunctionalExtensionality.vo
RTAUTOVO:= \
contrib/rtauto/Bintree.vo contrib/rtauto/Rtauto.vo