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

Changes for supporting ghost applications and ghost bind in Steel #3012

Merged
merged 25 commits into from
Aug 12, 2023
Merged

Changes for supporting ghost applications and ghost bind in Steel #3012

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
25 commits
Select commit Hold shift + click to select a range
b94e2d3
a type abbrev.
aseemr Aug 3, 2023
6cf786c
Merge branch 'master' of github.com:FStarLang/FStar
aseemr Aug 4, 2023
e4bb9b4
following stubs recipe to remove some duplication of tot_or_ghost
aseemr Aug 4, 2023
e6d6b94
snap
aseemr Aug 4, 2023
741ec81
same recipe for unfold_side
aseemr Aug 4, 2023
b5deac6
snap
aseemr Aug 4, 2023
2f87e46
wip
aseemr Aug 4, 2023
077a94c
merge with master
aseemr Aug 7, 2023
3efe473
merge with aseem_core_fix
aseemr Aug 7, 2023
8540f20
bootstrap
aseemr Aug 7, 2023
839195d
wip, API change
aseemr Aug 7, 2023
20e9d55
wip, API change
aseemr Aug 7, 2023
42e67d7
fix in non informative judgment
aseemr Aug 7, 2023
1dfbf74
scaffolding for an is_non_informative API
aseemr Aug 7, 2023
bc4c8a5
snap
aseemr Aug 7, 2023
6c5cd45
a non informative token rule
aseemr Aug 7, 2023
3ba5684
nit
aseemr Aug 7, 2023
f398473
snap
aseemr Aug 7, 2023
27f4fc2
allow ghost when lax checking for inferring implicits
aseemr Aug 7, 2023
8f156aa
snap
aseemr Aug 7, 2023
5599fcb
merge with master
aseemr Aug 8, 2023
1ed8a3d
some cleanup and comments
aseemr Aug 8, 2023
3acd7bb
snap
aseemr Aug 8, 2023
0154762
Merge branch 'master' into _aseem_ghost_v2
aseemr Aug 8, 2023
12997f0
Merge branch 'master' into _aseem_ghost_v2
nikswamy Aug 12, 2023
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
5 changes: 3 additions & 2 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 @@ -136,12 +136,13 @@ let free_uvars = from_tac_1 "B.free_uvars" B.free_uvars
type ('env, 't) prop_validity_token = unit
type ('env, 'sc, 't, 'pats, 'bnds) match_complete_token = unit

let is_non_informative = from_tac_2 "B.refl_is_non_informative" B.refl_is_non_informative
let check_subtyping = from_tac_3 "B.refl_check_subtyping" B.refl_check_subtyping
let check_equiv = from_tac_3 "B.refl_check_equiv" B.refl_check_equiv
let core_compute_term_type = from_tac_3 "B.refl_core_compute_term_type" B.refl_core_compute_term_type
let core_compute_term_type = from_tac_2 "B.refl_core_compute_term_type" B.refl_core_compute_term_type
let core_check_term = from_tac_4 "B.refl_core_check_term" B.refl_core_check_term
let check_match_complete = from_tac_4 "B.refl_check_match_complete" B.refl_check_match_complete
let tc_term = from_tac_3 "B.refl_tc_term" B.refl_tc_term
let tc_term = from_tac_2 "B.refl_tc_term" B.refl_tc_term
let universe_of = from_tac_2 "B.refl_universe_of" B.refl_universe_of
let check_prop_validity = from_tac_2 "B.refl_check_prop_validity" B.refl_check_prop_validity
let instantiate_implicits = from_tac_2 "B.refl_instantiate_implicits" B.refl_instantiate_implicits
Expand Down
124 changes: 67 additions & 57 deletions ocaml/fstar-lib/generated/FStar_Reflection_Typing.ml
View file
Open in desktop

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

Loading