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

Allow attributes on record fields #2192

Merged
Merged
Changes from 1 commit
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
4b7757a
allow more than one attributes on the binders
mateuszbujalski Dec 23, 2020
453849d
Enable attributes on non-implicit binders (needs fixing as it introdu…
mateuszbujalski Dec 30, 2020
e9a170f
Add support for attributes on record fields
mateuszbujalski Dec 30, 2020
4da1b26
snap
mateuszbujalski Dec 30, 2020
e9d1c67
fix test
mateuszbujalski Dec 30, 2020
1c502d9
drop outdated comment
mateuszbujalski Dec 30, 2020
ea76d8f
Add a test for attributes on explicit and implicit binders
mateuszbujalski Jan 11, 2021
e001b0c
Merge remote-tracking branch 'upstream/master' into matbuj_record_fie…
mateuszbujalski Jan 11, 2021
96a4994
regenerate parse.fsi
mateuszbujalski Jan 11, 2021
84f4bfa
Merge branch 'matbuj_record_field_attributes' of https://github.com/m…
nikswamy Feb 10, 2021
e2b0865
addressing conflicts in the grammar
nikswamy Feb 10, 2021
d3884c9
kick ci
nikswamy Feb 10, 2021
0f60de4
[@@@ for binder attributes
nikswamy Feb 10, 2021
a806100
update test cases to use @@@
nikswamy Feb 10, 2021
2c0d117
merging master in
nikswamy Feb 10, 2021
f464dbb
snap
nikswamy Feb 10, 2021
90164cf
snap
nikswamy Feb 10, 2021
2b3cd39
Remove todos as nik has fixed them
mateuszbujalski Feb 10, 2021
a1348cd
Merge remote-tracking branch 'upstream/master' into matbuj_record_fie…
mateuszbujalski Feb 11, 2021
97a9429
Add test for multiple attributes on a binder
mateuszbujalski Feb 12, 2021
23a90d8
Merge remote-tracking branch 'upstream/master' into matbuj_record_fie…
mateuszbujalski Feb 12, 2021
022d294
revert changes to FStar.Tactics.Util
mateuszbujalski Feb 12, 2021
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
6 changes: 4 additions & 2 deletions src/ocaml-output/FStar_Parser_AST.ml

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

8 changes: 6 additions & 2 deletions src/ocaml-output/FStar_Parser_Dep.ml

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

23 changes: 16 additions & 7 deletions src/ocaml-output/FStar_Parser_ToDocument.ml

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

17 changes: 16 additions & 1 deletion src/ocaml-output/FStar_Syntax_Resugar.ml

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

32 changes: 17 additions & 15 deletions src/ocaml-output/FStar_ToSyntax_ToSyntax.ml

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