remove hints

FStarLang · Jan 23, 2025 · bb5054d · bb5054d
1 parent 92316af
commit bb5054d
Show file tree

Hide file tree

Showing 161 changed files with 2 additions and 47,918 deletions.
diff --git a/lib/pulse/Pulse.Main.fsti.hints b/lib/pulse/Pulse.Main.fsti.hints
diff --git a/mk/test.mk b/mk/test.mk
@@ -23,7 +23,7 @@ include $(PULSE_ROOT)/mk/common.mk
 include $(PULSE_ROOT)/mk/locate.mk
 .DEFAULT_GOAL := all
 
-HINTS_ENABLED?=--use_hints
+HINTS_ENABLED?=
 
 # This warning is really useless.
 OTHERFLAGS += --warn_error -321

diff --git a/qs/fstar.mk b/qs/fstar.mk
@@ -24,7 +24,7 @@ FSTAR_EXE ?= fstar.exe
 $(call need_exe,FSTAR_EXE)
 export FSTAR_EXE
 
-HINTS_ENABLED?=--use_hints
+HINTS_ENABLED?=
 
 # This warning is really useless.
 OTHERFLAGS += --warn_error -321

diff --git a/src/checker/.hints/Pulse.ASTBuilder.fsti.hints b/src/checker/.hints/Pulse.ASTBuilder.fsti.hints
diff --git a/src/checker/.hints/Pulse.Checker.Abs.fst.hints b/src/checker/.hints/Pulse.Checker.Abs.fst.hints
diff --git a/src/checker/.hints/Pulse.Checker.Abs.fsti.hints b/src/checker/.hints/Pulse.Checker.Abs.fsti.hints
diff --git a/src/checker/.hints/Pulse.Checker.Admit.fst.hints b/src/checker/.hints/Pulse.Checker.Admit.fst.hints
diff --git a/src/checker/.hints/Pulse.Checker.Admit.fsti.hints b/src/checker/.hints/Pulse.Checker.Admit.fsti.hints