index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
Commit message (
Expand
)
Author
Age
*
Fix broken proofs
Jason Gross
2018-12-04
*
Add more Forall2 lemmas
Jason Gross
2018-12-04
*
Add more ListUtil Forall Lemmas
Jason Gross
2018-12-04
*
Yet more repeat fixing
Jason Gross
2018-12-04
*
More repeat fixing
Jason Gross
2018-12-04
*
Add some ListUtil lemmas about Forall2
Jason Gross
2018-12-04
*
Fix bugs introduced by previous commit
Jason Gross
2018-12-04
*
Remove ListUtil.List.repeat
Jason Gross
2018-12-04
*
Revert "Add inversion_clear tactics"
Jason Gross
2018-12-04
*
Add inversion_clear tactics
Jason Gross
2018-12-04
*
Add value_or_expr_interp_ok
Jason Gross
2018-11-29
*
Add unfold_value'_interp_arrow
Jason Gross
2018-11-28
*
Add value_interp_ok_{arrow,base}
Jason Gross
2018-11-28
*
Add some more rawexpr equiv lemmas
Jason Gross
2018-11-27
*
Add reveal_rawexpr_equiv
Jason Gross
2018-11-27
*
Restrict rawexpr_equiv to match with reveal better
Jason Gross
2018-11-27
*
Add value_interp_self_related_of_ok
Jason Gross
2018-11-27
*
Add some lemmas about subst
Jason Gross
2018-11-27
*
Refactor interpretation of values
Jason Gross
2018-11-27
*
Global Set Fast Name Printing
Jason Gross
2018-11-27
*
Add related_sigT_by_eq proper lemmas
Jason Gross
2018-11-19
*
Add more reserved notations
Jason Gross
2018-11-19
*
Fix bug in previous commit
Jason Gross
2018-11-16
*
Add related_sigT_by_eq
Jason Gross
2018-11-16
*
Add app_forall_vars_lam_forall_vars
Jason Gross
2018-11-16
*
Add some lemmas about wf value interp related
Jason Gross
2018-11-15
*
Add UnderLets.wf_interp_Proper
Jason Gross
2018-11-15
*
Add a couple of useful lemmas
Jason Gross
2018-11-15
*
Uncurry rewriter rules
Jason Gross
2018-11-15
*
Base Dead Code Elim on Subst01
Jason Gross
2018-11-15
*
Add support for parsing Q and bool
Jason Gross
2018-11-12
*
Add map_repeat, map_const
Jason Gross
2018-11-11
*
Update the post-bounds rewrite rules
Jason Gross
2018-11-11
*
Split off all of the arithmetic rules that need bounds info
Jason Gross
2018-11-11
*
parenthesize proofs in Weierstrass.Projective (closes #456)
Andres Erbsen
2018-11-11
*
Add a variant of cps_id that pulls the continuation from the lhs
Jason Gross
2018-11-08
*
Revert "Disable very very slow printing"
Jason Gross
2018-11-07
*
Fix the s-adjustment for saturated solinas
Jason Gross
2018-11-06
*
Disable very very slow printing
Jason Gross
2018-11-06
*
Revert "Factor out a common computation to fix n² behavior"
Jason Gross
2018-11-06
*
Factor out a common computation to fix n² behavior
Jason Gross
2018-11-06
*
Use a better strategy in Rows.sat_reduce
Jason Gross
2018-11-06
*
Restrict [ident.cast] a bit more
Jason Gross
2018-11-05
*
Add .out files for rewriter
Jason Gross
2018-11-02
*
Also inline Z_cast things
Jason Gross
2018-11-01
*
Add some zrange lemmas
Jason Gross
2018-11-01
*
Make pairs work in Z_cast2
Jason Gross
2018-11-01
*
Export ZRange operation notations
Jason Gross
2018-11-01
*
Add zrange notations
Jason Gross
2018-11-01
*
Fix a thing broken by previous commit
Jason Gross
2018-11-01
[next]