aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-04-03 15:01:47 -0400
committerGravatar Jason Gross <jasongross9@gmail.com>2017-04-07 13:36:36 -0400
commit9b5690a9c5db3c3650c3b4899745be551b3fe89e (patch)
treec1e73d288d0a117cd79ebf1b1e79f99dc3742edf /Makefile
parent3c75bd3f0e1106be0d238897c4df34ceb5dd811b (diff)
Add IntegrationTestLadderstep.v
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 36c8e0034..a2c33ed49 100644
--- a/Makefile
+++ b/Makefile
@@ -44,7 +44,7 @@ UNMADE_VOFILES := src/SpecificGen/% src/Specific/%Display.vo
# targets by the "lite" target
# N.B. if a file not in this list depends on one in this list,
# that file will be built by the "lite" target
-HEAVY_VOFILES := src/WeierstrassCurve/WeierstrassCurveTheorems.vo
+HEAVY_VOFILES := src/WeierstrassCurve/WeierstrassCurveTheorems.vo src/Specific/IntegrationTestLadderstep.vo
COQ_VOFILES := $(filter-out $(UNMADE_VOFILES),$(VOFILES))
LITE_VOFILES := $(filter-out $(HEAVY_VOFILES),$(COQ_VOFILES))