diff --git a/examples/algorithms/BinarySearch/BinarySearch.fsproj b/examples/algorithms/BinarySearch/BinarySearch.fsproj
index 2758b6d074e..011789ccae3 100644
--- a/examples/algorithms/BinarySearch/BinarySearch.fsproj
+++ b/examples/algorithms/BinarySearch/BinarySearch.fsproj
@@ -5,7 +5,7 @@
   <PropertyGroup>
     <FSTAR_HOME>..\..\..</FSTAR_HOME>
     <!-- Custom FStar flags used in this project . -->
-    <FSTAR_FLAGS>--use_hints --record_hints</FSTAR_FLAGS>
+    <FSTAR_FLAGS>--ext context_pruning</FSTAR_FLAGS>
   </PropertyGroup>
   <Import Project="$(FSTAR_HOME)\examples\fsharp.extraction.targets" />
   <ItemGroup>
diff --git a/examples/algorithms/Huffman/Huffman.fsproj b/examples/algorithms/Huffman/Huffman.fsproj
index 42687221fea..674f9d8b1e0 100644
--- a/examples/algorithms/Huffman/Huffman.fsproj
+++ b/examples/algorithms/Huffman/Huffman.fsproj
@@ -5,7 +5,7 @@
   <PropertyGroup>
     <FSTAR_HOME>..\..\..</FSTAR_HOME>
     <!-- Custom FStar flags used in this project . -->
-    <FSTAR_FLAGS>--use_hints --record_hints</FSTAR_FLAGS>
+    <FSTAR_FLAGS>--ext context_pruning</FSTAR_FLAGS>
   </PropertyGroup>
   <Import Project="$(FSTAR_HOME)\examples\fsharp.extraction.targets" />
   <ItemGroup>
diff --git a/examples/data_structures/Lens/Lens.fsproj b/examples/data_structures/Lens/Lens.fsproj
index 6e3cbf25a82..a06b155915e 100644
--- a/examples/data_structures/Lens/Lens.fsproj
+++ b/examples/data_structures/Lens/Lens.fsproj
@@ -5,7 +5,7 @@
   <PropertyGroup>
     <FSTAR_HOME>..\..\..</FSTAR_HOME>
     <!-- Custom FStar flags used in this project . -->
-    <FSTAR_FLAGS>--use_hints --record_hints</FSTAR_FLAGS>
+    <FSTAR_FLAGS>--ext context_pruning</FSTAR_FLAGS>
   </PropertyGroup>
   <Import Project="$(FSTAR_HOME)\examples\fsharp.extraction.targets" />
   <ItemGroup>
diff --git a/examples/dependencies/Makefile b/examples/dependencies/Makefile
index 123f0c90c1b..9139c4081ab 100644
--- a/examples/dependencies/Makefile
+++ b/examples/dependencies/Makefile
@@ -18,13 +18,10 @@ endif
 OUT_DIR   = out
 CACHE_DIR = cache
 ROOTS     = Test.fst
-HINT_DIR  = hints
 
 FSTAR_FLAGS = $(OTHERFLAGS) --cmi --odir $(OUT_DIR) --cache_dir $(CACHE_DIR) \
-  --cache_checked_modules --already_cached 'Prims FStar' --z3version 4.13.3
-
-# Run with ENABLE_HINTS= to disable
-ENABLE_HINTS ?= --use_hints
+  --cache_checked_modules --already_cached 'Prims FStar' --z3version 4.13.3 \
+  --ext context_pruning
 
 FSTAR = $(FSTAR_EXE) $(FSTAR_FLAGS)
 
@@ -44,7 +41,7 @@ all:
 include .depend
 
 $(CACHE_DIR)/%.checked:
-	$(FSTAR) $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $<).hints && \
+	$(FSTAR) $< && \
 	touch $@
 
 # 2. Compile all .ml files to .cmx and link them to get an executable
diff --git a/examples/hello/Hello/Hello.fsproj b/examples/hello/Hello/Hello.fsproj
index 5532e06a29a..c28bd0cc99e 100644
--- a/examples/hello/Hello/Hello.fsproj
+++ b/examples/hello/Hello/Hello.fsproj
@@ -8,7 +8,7 @@
   <PropertyGroup>
     <FSTAR_HOME>..\..\..</FSTAR_HOME>
     <!-- Custom FStar flags used in this project -->
-    <FSTAR_FLAGS>--use_hints --record_hints</FSTAR_FLAGS>
+    <FSTAR_FLAGS>--ext context_pruning</FSTAR_FLAGS>
   </PropertyGroup>
   <Import Project="$(FSTAR_HOME)\examples\fsharp.extraction.targets" />
   <ItemGroup>
diff --git a/examples/hello/TestFSharp/TestFSharp.fsproj b/examples/hello/TestFSharp/TestFSharp.fsproj
index d8c1fa04176..c260afb85e1 100644
--- a/examples/hello/TestFSharp/TestFSharp.fsproj
+++ b/examples/hello/TestFSharp/TestFSharp.fsproj
@@ -6,7 +6,7 @@
   <PropertyGroup>
     <FSTAR_HOME>..\..\..</FSTAR_HOME>
     <!-- Custom FStar flags used in this project -->
-    <FSTAR_FLAGS>--use_hints --record_hints</FSTAR_FLAGS>
+    <FSTAR_FLAGS>--ext context_pruning</FSTAR_FLAGS>
   </PropertyGroup>
   <Import Project="$(FSTAR_HOME)\examples\fsharp.extraction.targets" />
   <ItemGroup>
diff --git a/examples/old/tls-record-layer/Makefile b/examples/old/tls-record-layer/Makefile
index 3d63b057ef7..bf4a67cf2bf 100644
--- a/examples/old/tls-record-layer/Makefile
+++ b/examples/old/tls-record-layer/Makefile
@@ -177,13 +177,13 @@ chacha-aead-test: chacha-aead-compile
 	./test_chacha_aead.exe
 
 bignum-ver:
-	$(FSTAR) --use_hints crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part1.fst --include crypto
-	$(FSTAR) --use_hints crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part2.fst --include crypto
-	$(FSTAR) --use_hints crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part3.fst --include crypto
-	$(FSTAR) --use_hints crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part4.fst --include crypto
-	$(FSTAR) --use_hints crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part5.fst --include crypto
-	$(FSTAR) --use_hints crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part6.fst --include crypto
-	$(FSTAR) --use_hints --include crypto crypto/Crypto.Symmetric.Poly1305.Bignum.fst
+	$(FSTAR) --ext context_pruning crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part1.fst --include crypto
+	$(FSTAR) --ext context_pruning crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part2.fst --include crypto
+	$(FSTAR) --ext context_pruning crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part3.fst --include crypto
+	$(FSTAR) --ext context_pruning crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part4.fst --include crypto
+	$(FSTAR) --ext context_pruning crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part5.fst --include crypto
+	$(FSTAR) --ext context_pruning crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part6.fst --include crypto
+	$(FSTAR) --ext context_pruning --include crypto crypto/Crypto.Symmetric.Poly1305.Bignum.fst
 
 KRML_INCLUDES=$(addprefix -I ,spartan_aes crypto $(KRML_HOME)/krmllib $(KRML_HOME)/test)
 ifeq ($(OS),Windows_NT)
diff --git a/examples/old/tls-record-layer/crypto/Makefile b/examples/old/tls-record-layer/crypto/Makefile
index 02fce713ebd..3310c38bd6b 100644
--- a/examples/old/tls-record-layer/crypto/Makefile
+++ b/examples/old/tls-record-layer/crypto/Makefile
@@ -2,9 +2,7 @@ FSTAR_HOME=../../..
 
 FSTAR?=$(FSTAR_HOME)/bin/fstar.exe
 
-HINTS_ENABLED?=--use_hints
-
-OPTIONS=--fstar_home $(FSTAR_HOME) --max_fuel 4 --initial_fuel 0 --max_ifuel 2 --initial_ifuel 0 --z3rlimit 20  $(HINTS_ENABLED) $(OTHERFLAGS)
+OPTIONS=--fstar_home $(FSTAR_HOME) --max_fuel 4 --initial_fuel 0 --max_ifuel 2 --initial_ifuel 0 --z3rlimit 20 --ext context_pruning $(OTHERFLAGS)
 
 FSTAR_INCLUDE_PATHS=--include $(FSTAR_HOME)/ulib/hyperstack --include hacl
 
diff --git a/examples/sample_project/Makefile b/examples/sample_project/Makefile
index 3a296d5ba64..fb02b75078e 100644
--- a/examples/sample_project/Makefile
+++ b/examples/sample_project/Makefile
@@ -14,7 +14,7 @@ TOP_LEVEL_FILE=ml/main.ml
 OUTPUT_DIRECTORY=_output
 
 ################################################################################
-FSTAR=fstar.exe --cache_checked_modules --odir $(OUTPUT_DIRECTORY) --use_hints $(OTHERFLAGS)
+FSTAR=fstar.exe --cache_checked_modules --odir $(OUTPUT_DIRECTORY) --ext context_pruning $(OTHERFLAGS)
 ML_FILES=$(addprefix $(OUTPUT_DIRECTORY)/,$(addsuffix .ml,$(subst .,_, $(subst .fst,,$(FSTAR_FILES)))))
 OCAML_EXE=$(PROGRAM).ocaml.exe
 KRML_EXE=$(PROGRAM).exe
diff --git a/mk/lib.mk b/mk/lib.mk
index 3553e4344e2..3e602dc8360 100644
--- a/mk/lib.mk
+++ b/mk/lib.mk
@@ -1,6 +1,3 @@
-FSTAR_OPTIONS += --use_hints
-FSTAR_OPTIONS += --hint_dir $(SRC)/.hints
-FSTAR_OPTIONS += --warn_error -333 # Do not warn about missing hints
 FSTAR_OPTIONS += --ext context_pruning
 FSTAR_OPTIONS += --z3version 4.13.3
 
diff --git a/mk/test.mk b/mk/test.mk
index 43729b3d01a..17298791dd5 100644
--- a/mk/test.mk
+++ b/mk/test.mk
@@ -27,8 +27,6 @@ FSTAR_EXE ?= $(FSTAR_ROOT)/out/bin/fstar.exe
 FSTAR_EXE := $(abspath $(FSTAR_EXE))
 export FSTAR_EXE
 
-HINTS_ENABLED?=--use_hints
-
 # This warning is really useless.
 OTHERFLAGS += --warn_error -321
 OTHERFLAGS += --ext context_pruning
@@ -50,7 +48,7 @@ FSTAR = $(FSTAR_EXE) $(SIL) 				\
 	--odir $(OUTPUT_DIR)				\
 	--cache_dir $(CACHE_DIR)			\
 	--already_cached Prims,FStar,LowStar		\
-	 $(OTHERFLAGS) $(MAYBE_ADMIT) $(HINTS_ENABLED)
+	 $(OTHERFLAGS) $(MAYBE_ADMIT)
 
 ifneq ($(MAKECMDGOALS),clean)
 ifeq ($(NODEPEND),) # Set NODEPEND=1 to not dependency analysis
diff --git a/stage0/ulib/Makefile.verify b/stage0/ulib/Makefile.verify
index 9f8c2a12667..afd2553ab7e 100644
--- a/stage0/ulib/Makefile.verify
+++ b/stage0/ulib/Makefile.verify
@@ -28,7 +28,7 @@ FSTAR_FILES += $(filter-out $(FLAKY), \
 endif
 endif
 
-WITH_CACHE_DIR=--cache_dir .cache --hint_dir .hints
+WITH_CACHE_DIR=--cache_dir .cache
 
 # 271 -> pattern uses theory symbols
 # 330 -> experimental feature
@@ -43,7 +43,6 @@ include gmake/Makefile.tmpl
 # Default rule is verify-all, defined in gmake/Makefile.tmpl
 
 %.fst-in:
-	@echo --use_hints --hint_info
 
 #turn off 271 (pattern uses theory symbols warning), to be fixed soon
 %FStar.UInt.fsti.checked: OTHERFLAGS+=--warn_error -271
diff --git a/stage0/ulib/gmake/fstar.mk b/stage0/ulib/gmake/fstar.mk
index 9e167be180a..edd1db1abd8 100644
--- a/stage0/ulib/gmake/fstar.mk
+++ b/stage0/ulib/gmake/fstar.mk
@@ -1,4 +1,3 @@
-HINTS_ENABLED?=--use_hints
 WARN_ERROR=
 OTHERFLAGS+=$(WARN_ERROR)
 OTHERFLAGS+=--z3version 4.13.3
@@ -20,7 +19,7 @@ else
 # FSTAR_HOME not defined, assume fstar.exe reachable from PATH
 FSTAR_EXE?=fstar.exe
 endif
-FSTAR=$(FSTAR_EXE) $(OTHERFLAGS) $(MAYBE_ADMIT) $(HINTS_ENABLED) $(WITH_CACHE_DIR)
+FSTAR=$(FSTAR_EXE) $(OTHERFLAGS) $(MAYBE_ADMIT) $(WITH_CACHE_DIR)
 
 # Benchmarking wrappers are enabled by setting BENCHMARK_CMD, for example:
 #  make -C tests/micro-benchmarks BENCHMARK_CMD=time