index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Generalize BoundByCast a bit
Jason Gross
2017-02-10
*
Add EtaInterp, EtaWf
Jason Gross
2017-02-10
*
Use Eta in BoundByCast
Jason Gross
2017-02-10
*
Add Reflection/Eta.v
Jason Gross
2017-02-10
*
Fix a missing section close in ZToRing
Jason Gross
2017-02-10
*
Add files for constant reflective notations
Jason Gross
2017-02-10
*
Accidentally pushed wrong file in last commit; this is the correct one
jadep
2017-02-10
*
added ZToRing to _CoqProject
jadep
2017-02-09
*
Added ZToRing lemmas
jadep
2017-02-09
*
Remove useless imports
Jason Gross
2017-02-08
*
Factor things into BoundByCast.v
Jason Gross
2017-02-08
*
Fix type inference bug in 8.6
Jason Gross
2017-02-08
*
Simpler version of MapCast
Jason Gross
2017-02-08
*
Remove the let-in from SmartValf
Jason Gross
2017-02-07
*
Fix relation relb arguments
Jason Gross
2017-02-07
*
Add things like interp_flat_type_rel_pointwise1_gen_Prop_iff_bool
Jason Gross
2017-02-07
*
Clean up and improve Reflection.Relations
Jason Gross
2017-02-07
*
Add ZUtil lemmas
Jason Gross
2017-02-06
*
Add interp_flat_type_rel_pointwise2_flatten_binding_list
Jason Gross
2017-02-06
*
Move things from WordUtil to ZUtil, add word lemma
Jason Gross
2017-02-06
*
field_nsatz
Andres Erbsen
2017-02-06
*
Fix changed names
Jason Gross
2017-02-03
*
Split off non-unfolding version of fixed_size_op_to_word
Jason Gross
2017-02-03
*
Add valid_update lemmas about FixedWordSizes
Jason Gross
2017-02-03
*
Don't unfold wordToZ_gen in fixed_Size_op_to_word
Jason Gross
2017-02-03
*
More zutil
Jason Gross
2017-02-03
*
Add lemmas about bounds of Z.lor, and add Z.max_log2_up
Jason Gross
2017-02-03
*
Fix a missing argument
Jason Gross
2017-02-03
*
Fix a typo
Jason Gross
2017-02-03
*
Handle more kinds of ops in fixed_size_op_to_word
Jason Gross
2017-02-03
*
Only unfold the non-zpecialized versions of wcmovl, wcmovne, wneg
Jason Gross
2017-02-03
*
Also unfold wcmovl, wcmovne, wneg in fixed_size_constants
Jason Gross
2017-02-03
*
Don't autounfold wordToZ nor ZToWord
Jason Gross
2017-02-03
*
Add fixed_size_op_to_word tactic
Jason Gross
2017-02-03
*
Add interp_flat_type_rel_pointwise2_hetero_iff
Jason Gross
2017-02-03
*
Add lemmas for Z ops Proper
Jason Gross
2017-02-03
*
Add log2_up_le_full
Jason Gross
2017-02-03
*
Add Z.log2_up_nonneg to zarith
Jason Gross
2017-02-03
*
Reorder Reflection.Z.Syntax
Jason Gross
2017-02-02
*
Split up Reflection/Z/Syntax and make it smaller
Jason Gross
2017-02-02
*
Add wf database
Jason Gross
2017-02-01
*
Generalize InlineInterp
Jason Gross
2017-02-01
*
Fix lazymatch ordering
Jason Gross
2017-02-01
*
More powerful preinvert_one_type
Jason Gross
2017-02-01
*
Add wordToZ_ZToWord_wordToZ
Jason Gross
2017-02-01
*
Add ZToWord_wordToZ_ZToWord
Jason Gross
2017-02-01
*
Add NToWord_wordToN_NToWord
Jason Gross
2017-02-01
*
Add wordToZ_ZToWord, ZToWord_wordToZ
Jason Gross
2017-02-01
*
Add invert_match_op
Jason Gross
2017-02-01
*
Add invert_op
Jason Gross
2017-02-01
[next]