Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Misc tactics and debugging improvements #3300

Merged
merged 10 commits into from
May 21, 2024
Merged

Misc tactics and debugging improvements #3300

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
c6e8e18
Tc: pretty printing basic_type_error
mtzguido Sep 29, 2023
8257736
Tactics: add a ForceSMT guard_policy
mtzguido May 17, 2024
74e4ded
Tactics: nit on debug message
mtzguido May 17, 2024
ea6f6af
Tactics: minor refactor
mtzguido May 17, 2024
6a082fa
Syntax.Free: use a binary operator for union
mtzguido May 20, 2024
dcdda27
Syntax.Free: consider vars in residual comp of match
mtzguido May 20, 2024
3da0899
Tactics: adding a norm_well_typed_term reflection call
mtzguido May 20, 2024
2b7166e
SMTEncoding: introduce --debug SMTFail to print a diagnostic for fail…
mtzguido May 20, 2024
3c11db4
snap
mtzguido May 21, 2024
047e0fe
Update expected output
mtzguido May 21, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions ocaml/fstar-lib/FStar_Tactics_V2_Builtins.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -155,6 +155,8 @@ let instantiate_implicits = from_tac_2 "B.refl_instantiate_implicits" B.r
let try_unify = from_tac_4 "B.refl_try_unify" B.refl_try_unify
let maybe_relate_after_unfolding = from_tac_3 "B.refl_maybe_relate_after_unfolding" B.refl_maybe_relate_after_unfolding
let maybe_unfold_head = from_tac_2 "B.refl_maybe_unfold_head" B.refl_maybe_unfold_head
let norm_well_typed_term = from_tac_3 "B.norm_well_typed_term" B.refl_norm_well_typed_term

let push_open_namespace = from_tac_2 "B.push_open_namespace" B.push_open_namespace
let push_module_abbrev = from_tac_3 "B.push_module_abbrev" B.push_module_abbrev
let resolve_name = from_tac_2 "B.resolve_name" B.resolve_name
Expand Down
75 changes: 45 additions & 30 deletions ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

126 changes: 72 additions & 54 deletions ocaml/fstar-lib/generated/FStar_Syntax_Free.ml
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Loading
Loading