From 7cb8c8a6724feb303eb1a49452c012738bdd48ef Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= <theophile@wallez.net>
Date: Thu, 17 Oct 2024 09:54:19 +0200
Subject: [PATCH] build: use context pruning

---
 Makefile | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index 8365031..61c02e7 100644
--- a/Makefile
+++ b/Makefile
@@ -67,11 +67,12 @@ obj:
 
 %.checked: FSTAR_RULE_FLAGS=
 
+#
+cache/MLS.%.checked: FSTAR_RULE_FLAGS = --ext context_pruning
 # MLS.Test is the only file allowing "(Warning 272) Top-level let-bindings must be total; this term may have effects"
 cache/MLS.Test.fst.checked: FSTAR_RULE_FLAGS = --warn_error '+272'
 # Allow more warning in dependencies
 cache/Lib.IntTypes.fst.checked: FSTAR_RULE_FLAGS = --warn_error '+288+349'
-cache/DY.Core.Bytes.Type.fst.checked: FSTAR_RULE_FLAGS = --warn_error '+290'
 
 %.checked: | hints obj
 	$(FSTAR) $(FSTAR_FLAGS) $(FSTAR_RULE_FLAGS) $< && touch -c $@