aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile1
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index f9d64ac83..2cb11476c 100644
--- a/Makefile
+++ b/Makefile
@@ -87,6 +87,7 @@ LITE_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo \
src/Specific/X25519/C32/fe%.vo \
src/Experiments/NewPipeline/Toplevel2.vo \
src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo \
+ src/Experiments/SimplyTypedArithmetic.vo \
$(SPECIFIC_GENERATED_VOFILES)
NOBIGMEM_UNMADE_VOFILES := \
src/Curves/Weierstrass/AffineProofs.vo \