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
*
Add some more underlets lemmas
Jason Gross
2019-04-04
*
Add UnderLets flat_map interp proofs,other changes
Jason Gross
2019-04-04
*
partition -> Partition.partition to prevent confusion with List.partition
jadep
2019-04-03
*
fix typo
jadep
2019-04-03
*
remove unnecessary imports from Primitives.v
jadep
2019-04-03
*
fix up imports in SmallExamples.v
jadep
2019-04-03
*
update import statements
jadep
2019-04-03
*
rename some things
jadep
2019-04-03
*
fix imports and qualifiers so everything builds
jadep
2019-04-03
*
remove extraneous module identifiers
jadep
2019-04-03
*
update _CoqProject, fix indentations, and prune dependencies of new Arithmeti...
jadep
2019-04-03
*
split up Arithmetic (imports etc. not yet fixed, does not build)
jadep
2019-04-03
*
Add Z.combine_at_bitwidth
Jason Gross
2019-04-02
*
Factor out rewriter rules
Jason Gross
2019-03-31
*
Fix a non-terminated comment
Jason Gross
2019-03-31
*
Add some comments based on CR requests
Jason Gross
2019-03-31
*
Fix issue with refolding in eapply in < 8.9
Jason Gross
2019-03-31
*
Finish reifying list lemmas
Jason Gross
2019-03-31
*
Add constr_fail and constr_fail_with
Jason Gross
2019-03-31
*
improve zero_bounds tactic
jadep
2019-03-26
*
add some hints to the global databases
jadep
2019-03-26
*
remove Derive to fix 8.7
jadep
2019-03-25
*
fix montgomery
jadep
2019-03-25
*
remove 2: syntax so I don't break 8.7
jadep
2019-03-25
*
fix up a messy proof
jadep
2019-03-25
*
Move some lemmas to appropriate places
jadep
2019-03-25
*
finish proofs
jadep
2019-03-25
*
Get new Barrett proofs to generate Fancy code as before
jadep
2019-03-25
*
WIP
jadep
2019-03-25
*
Add UnderLets.wf_flat_map
Jason Gross
2019-03-12
*
Add UnderLets.wf_of_expr
Jason Gross
2019-03-09
*
Add some UnderLets wf proofs
Jason Gross
2019-03-08
*
Standardize list wf things
Jason Gross
2019-03-08
*
Add Forall2_Proper instances
Jason Gross
2019-03-08
*
Add Forall2_map_map_iff
Jason Gross
2019-03-08
*
Add wf_reify_list_Forall2
Jason Gross
2019-03-08
*
Allow more reucrsion in wf_safe_t_step
Jason Gross
2019-03-08
*
Fix issue with previous commit
Jason Gross
2019-03-08
*
Add some eq list_rect lemmas to ListUtil
Jason Gross
2019-03-08
*
Add eager_nth_default
Jason Gross
2019-03-08
*
Remove GlobalTacticals
Jason Gross
2019-03-08
*
Fix grepeat tactic
Jason Gross
2019-03-08
*
Fix gprogress tactical
Jason Gross
2019-03-08
*
Add some gtactics
Jason Gross
2019-03-08
*
Fix a typo
Jason Gross
2019-03-08
*
add wf_smart_Literal_eq
Jason Gross
2019-03-08
*
Add wf_smart_Literal
Jason Gross
2019-03-08
*
Add Forall2_forall_In_combine_iff
Jason Gross
2019-03-07
*
Add wf proofs to UnderLetsProofs
Jason Gross
2019-03-07
*
Fix hypothesis of UnderLets.list_rect_arrow_interp_related
Jason Gross
2019-03-07
[next]