| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* [demo] Add reification in src/Experiments/SimplyTypedArithmetic.v
It's rather verbose, unfortunately. The reification also doesn't have
any of the nice debugging features of the version of reification in
Compilers, because that's even more boilerplate. Not sure if I should
add that back in, at the moment.
Also, for some strange reason, places where `constr`s fail to typecheck
seem to induce backtracking where I don't think they should, and I'm not
sure what's going on...
* [demo] Add more namespacing
* Update llet notation, update is_known_const name
As per code review suggestions
* Namespace var_context, add some coqbug references
* Rename is_type_arg to is_template_parameter
As per https://github.com/mit-plv/fiat-crypto/pull/275#discussion_r153036059
* Simplify the logic around delayed arguments a bit
We no longer pass around dummy markers in the tuple of arguments.
* [demo] More informative reification error messages
This time without exponential slowdown in failure cases and without
needing to manually think up all of the possible errors and write them
out.
Possible thanks to Hugo's comment at
https://github.com/coq/coq/issues/6252#issuecomment-347041995
* [demo] respond to code review, add comments
* Update documentation with suggestions from Andres
|
|
|
|
| |
As per https://github.com/mit-plv/fiat-crypto/pull/275#discussion_r153084144
|
|
|
|
| |
This sets the level and associativity in a common place, and will be useful for PHOAS application nodes
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
This will make it easier to reify
|
|
|
|
|
| |
As per
https://github.com/mit-plv/fiat-crypto/pull/271/commits/76634efa66aa9085a1e410c04f930dd5645126df#r152719891
|
|
|
|
|
|
|
| |
As per
https://github.com/mit-plv/fiat-crypto/pull/271/commits/76634efa66aa9085a1e410c04f930dd5645126df#r152720364
and
https://github.com/mit-plv/fiat-crypto/pull/271/commits/76634efa66aa9085a1e410c04f930dd5645126df#r152720444
|
| |
|
|
|
|
|
| |
As per
https://github.com/mit-plv/fiat-crypto/pull/271#discussion_r152720545
|
| |
|
|
|
|
|
|
|
| |
This is preparing the landing of https://github.com/coq/coq/pull/1049.
For now, I'm duplicating this patch which was already done upstream in
CoqPrime, but please consider removing this ad-hoc copy (see discussion
on PR #269).
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
It's currently a bit ad-hoc, and relies on the presence of git to add
things to _CoqProject, but it's a bit better than manually invoking the
commands. More refinements to come, hopefully.
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
| |
Formatting
|
| |
|
| |
|
|
|
| |
Add a first draft of pointers to navigating the repo.
|