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.

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

Fixes for typeclasses #3134

Merged
merged 30 commits into from
Dec 5, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
30 commits
Select commit Hold shift + click to select a range
d369011
nit: more show instances
mtzguido Dec 3, 2023
b3cdabf
Tc: Rel: nit, use show
mtzguido Dec 3, 2023
4b2016e
Tc: Rel: trying to delay meta-args that have uvars in their type or env
mtzguido Dec 3, 2023
ab61854
Tc: setting a better internal reason for typeclass implicits
mtzguido Dec 3, 2023
497d581
Tc: Rel: in flex-flex quasi, retain meta-tac from the LHS
mtzguido Dec 3, 2023
8e9f09a
Update tests
mtzguido Dec 3, 2023
5a41382
snap
mtzguido Dec 3, 2023
f7f5aa5
Rel: never run meta-args in unresolved contexts
mtzguido Dec 4, 2023
865e724
Update tests
mtzguido Dec 4, 2023
833ec1f
snap
mtzguido Dec 4, 2023
82c0c9a
Class.Show: add instance for sets
mtzguido Dec 4, 2023
ce43a2d
Tc: another improved reason message for constraints
mtzguido Dec 4, 2023
0baba39
Add a test
mtzguido Dec 4, 2023
866e3c0
Tc: do not force trivial guard when checking attributes
mtzguido Dec 4, 2023
4f08036
Tc: fix typo
mtzguido Dec 4, 2023
6826645
Tc: Gen: improve error message
mtzguido Dec 4, 2023
56f628d
Tc: Gen: do not generalize implicits that have a meta
mtzguido Dec 4, 2023
fd2fe0c
snap
mtzguido Dec 4, 2023
eb3a541
Syntax/Tc: show instance for bindings/gamma
mtzguido Dec 5, 2023
ba86538
Add repro for #1066, somehow missing
mtzguido Dec 5, 2023
e37da50
Typeclass: more debug
mtzguido Dec 5, 2023
0bf2bc4
nit: show instances
mtzguido Dec 4, 2023
84401cf
Tc: Gen: don't fail due to unresolved non-Type implicits
mtzguido Dec 5, 2023
92bc8c3
Tc: running meta args in uvar's env, not the original env
mtzguido Dec 4, 2023
e01a065
Update tests + expected output
mtzguido Dec 5, 2023
b1024b8
snap
mtzguido Dec 5, 2023
2b22888
Syntax: remove traces of env in Ctx_uvar_meta_tac
mtzguido Dec 5, 2023
faed603
Bump checked file version
mtzguido Dec 5, 2023
bbbcff1
snap
mtzguido Dec 5, 2023
a01072d
Merge branch 'master' into 3130
mtzguido Dec 5, 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
21 changes: 20 additions & 1 deletion ocaml/fstar-lib/generated/FStar_CheckedFiles.ml

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

2 changes: 2 additions & 0 deletions ocaml/fstar-lib/generated/FStar_Class_Show.ml

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

14 changes: 7 additions & 7 deletions ocaml/fstar-lib/generated/FStar_Parser_Dep.ml

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

23 changes: 22 additions & 1 deletion ocaml/fstar-lib/generated/FStar_Syntax_Print.ml

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

5 changes: 2 additions & 3 deletions ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml

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

Loading