aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar jadep <jadep@mit.edu>2019-04-02 07:49:39 -0400
committerGravatar jadephilipoom <jade.philipoom@gmail.com>2019-04-03 23:34:53 +0100
commit291e80d252b476870ab01becfb9cd60b885f4e53 (patch)
tree66d51a2eb207cdcbc2e43ece641a0dd8db83bb19
parentc5565d1441e4882c9b4bc7181f745b4235d8353c (diff)
fix Makefile (old Arithmetic.v was hardcoded as a target)
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 62b318f29..42556fcf3 100644
--- a/Makefile
+++ b/Makefile
@@ -60,7 +60,7 @@ REGULAR_VOFILES := $(filter-out $(SPECIAL_VOFILES),$(VOFILES))
PRE_STANDALONE_PRE_VOFILES := $(filter src/Standalone%.vo,$(REGULAR_VOFILES))
UTIL_PRE_VOFILES := $(filter bbv/%.vo src/Algebra/%.vo src/Tactics/%.vo src/Util/%.vo,$(REGULAR_VOFILES))
SOME_EARLY_VOFILES := \
- src/Arithmetic.vo \
+ src/Arithmetic/Core.vo \
src/Rewriter.vo
# computing the vo_reverse_closure is slow, so we only do it if we're