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

Start a Tactics V2 #2960

Merged
merged 47 commits into from
Jun 19, 2023
Merged

Start a Tactics V2 #2960

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
47 commits
Select commit Hold shift + click to select a range
e339492
syntax: simplifying some embeddings, auto embeddings for @@plugin types
mtzguido Jun 11, 2023
0483dd1
embedding
mtzguido Jun 11, 2023
20272fe
reflection/tactics: Introduce V2
mtzguido Jun 11, 2023
21da63d
ulib: upgrade to syntax v2
mtzguido Jun 11, 2023
c01cc79
examples/tests: update to syntax v2
mtzguido Jun 11, 2023
22f72d3
snap
mtzguido Jun 11, 2023
6d1247b
WIP: Need to point to karamel fork
mtzguido Jun 11, 2023
8c42f2d
reflection: remove `exp` type from Reflection.Data
mtzguido Jun 12, 2023
aa0274d
snap
mtzguido Jun 12, 2023
606b34e
ulib: a rule to generate depgraphs for individual modules
mtzguido Jun 11, 2023
079a674
NamedView: do not use FStar.Option, reduce deps
mtzguido Jun 12, 2023
a219f3a
snap
mtzguido Jun 12, 2023
be03d18
remove some leftover admits
mtzguido Jun 12, 2023
9f6556c
syntax: introduce DT internally
mtzguido Jun 12, 2023
af31e12
snap
mtzguido Jun 12, 2023
ecebbeb
Merge branch 'master' of github:FStarLang/FStar into guido_syntax
mtzguido Jun 12, 2023
2704b2d
snap
mtzguido Jun 13, 2023
7d2526c
Merge branch 'master' of github:FStarLang/FStar into guido_syntax
mtzguido Jun 13, 2023
af69f99
ulib: move `unseal` into a new module FStar.Tactics.Unseal
mtzguido Jun 12, 2023
0f7fd9a
snap
mtzguido Jun 13, 2023
010539b
reflection: move `decls` into Types
mtzguido Jun 13, 2023
6a6ac2d
FStar.Tactics.Typeclasses: add an interface
mtzguido Jun 13, 2023
2e9843c
snap
mtzguido Jun 13, 2023
2c56ba6
fix
mtzguido Jun 13, 2023
295d767
Merge branch 'master' of github:FStarLang/FStar into guido_syntax
mtzguido Jun 15, 2023
4012c0e
tc/tactics: Introduce user-defined coercions via @@coercion attribute
mtzguido Jun 14, 2023
00a8dd6
ulib: syntax coercions (v2)
mtzguido Jun 14, 2023
7e23fe8
ulib: taking advantage of coercions
mtzguido Jun 14, 2023
c4e2bfb
tacv2: inspect/pack are coercions, restore test
mtzguido Jun 14, 2023
aa0747c
snap
mtzguido Jun 14, 2023
c758ae1
tests: add coercions tests
mtzguido Jun 14, 2023
b59547a
line number changed
mtzguido Jun 14, 2023
8158766
Makefile.common: use --output_deps_to
mtzguido Jun 14, 2023
06cef84
fix test
mtzguido Jun 15, 2023
c6a1fd8
fix snap
mtzguido Jun 15, 2023
2ebec50
Merge branch 'master' of github:FStarLang/FStar into guido_syntax
mtzguido Jun 15, 2023
cafe0a0
extraction: fix __range embedding
mtzguido Jun 15, 2023
9f9da6c
Tactics.NamedView: add an interface
mtzguido Jun 15, 2023
a0f0a9d
snap
mtzguido Jun 15, 2023
ad18b22
Tactics: expose close_term, Steel uses it
mtzguido Jun 15, 2023
6b56e36
snap
mtzguido Jun 15, 2023
0ca55b8
ci/docker: point back to upstream karamel repo
mtzguido Jun 18, 2023
a1e3a0a
Makefile.boot: extract FStar.Compiler namespace by default
mtzguido Jun 17, 2023
4040720
extraction: extract the FStar.Stubs.* namespace to FStar.*
mtzguido Jun 19, 2023
b1a8150
ulib: rename FStar.Syntax.Syntax -> FStar.Stubs.Syntax.Syntax
mtzguido Jun 19, 2023
cfcd88e
snap
mtzguido Jun 19, 2023
ba79fe2
hints
mtzguido Jun 19, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
20 changes: 10 additions & 10 deletions doc/book/code/AdHocEffectPolymorphism.fst.hints
View file
Open in desktop

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

28 changes: 14 additions & 14 deletions doc/book/code/Alex.fst.hints
View file
Open in desktop

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

16 changes: 8 additions & 8 deletions doc/book/code/AlexOpaque.fst.hints
View file
Open in desktop

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

Loading