Skip to content

Commit 1006c12

Browse files
committed
Allow #push-options "--lax"
1 parent f14e830 commit 1006c12

2 files changed

Lines changed: 2 additions & 1 deletion

File tree

src/basic/FStarC.Options.fst

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1761,6 +1761,7 @@ let settable = function
17611761
| "ide_id_info_off"
17621762
| "keep_query_captions"
17631763
| "lang_extensions"
1764+
| "lax"
17641765
| "load"
17651766
| "load_cmxs"
17661767
| "log_queries"

tests/tactics/Admit.fst

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ module Admit
22

33
open FStar.Tactics.V2
44

5-
#push-options "--admit_smt_queries true"
5+
#push-options "--lax"
66
let test () : squash False =
77
_ by (
88
()

0 commit comments

Comments
 (0)