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
*
Make a single tactic to build the rewriter
Jason Gross
2019-04-11
*
Automate more of the rewriter, and factor out rule-specific things
Jason Gross
2019-04-11
*
Add base.reflect_{base,type}_beq and type.reflect_type_beq
Jason Gross
2019-04-10
*
Fix for Coq 8.8
Jason Gross
2019-04-09
*
Automate more of the rewriter reification, proof
Jason Gross
2019-04-09
*
Fix for 8.8
Jason Gross
2019-04-05
*
Generalize correctly in strip_literal_casts_rewrite_rulesT
Jason Gross
2019-04-05
*
Add some bool eqb lemmas
Jason Gross
2019-04-05
*
Don't eagerly unfold boolean functions, hopefully, in tc reflect search
Jason Gross
2019-04-05
*
Hint reflect on negb
Jason Gross
2019-04-05
*
Add interp_related lemmas
Jason Gross
2019-04-05
*
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
[next]