index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Util
Commit message (
Expand
)
Author
Age
*
Factor out fold_right_cps2_specialized_step, add mapi_with'_cps2
Jason Gross
2017-10-22
*
Add curry{3,4}
Jason Gross
2017-10-20
*
Switch arithmetic to cps for Z * Z under the hood
Jason Gross
2017-10-19
*
Add mul_split_cps'
Jason Gross
2017-10-19
*
Update ZUtil cps definitions
Jason Gross
2017-10-19
*
Add ZUtil.CPS
Jason Gross
2017-10-19
*
Add 8.7-only CacheTerm
Jason Gross
2017-10-18
*
Add a Require Import FunInd (Function isn't loaded by default anymore)
Pierre Letouzey
2017-10-18
*
Allow instantiating type arguments without reducing matches
Jason Gross
2017-10-18
*
Allow instantiating type arguments without reducing matches
Jason Gross
2017-10-17
*
Allow instantiating type arguments without reducing matches
Jason Gross
2017-10-17
*
Allow instantiation of cps type arguments by unfolding
Jason Gross
2017-10-17
*
Add CacheTerm
Jason Gross
2017-10-17
*
Allow unfolding of mapi_with_cps to specialize the function to the type argum...
Jason Gross
2017-10-17
*
Work around bug #5341
Jason Gross
2017-10-17
*
Add strip_subst_local
Jason Gross
2017-10-15
*
Add pow_ceil_mul_nat_divide_upperbound
Jason Gross
2017-10-13
*
Add reflective compose, notation for Z.Syntax.{Expr,Interp}
Jason Gross
2017-10-12
*
Add update_by_tac_if_not_exists
Jason Gross
2017-10-10
*
TagList: make get error, and fix bugs
Jason Gross
2017-10-10
*
Add TagList
Jason Gross
2017-10-10
*
Add notations
Jason Gross
2017-10-10
*
Add pow_ceil_mul_nat_nonneg
Jason Gross
2017-10-05
*
Add PoseTermWithName
Jason Gross
2017-10-05
*
Add some ZUtil lemmas
Jason Gross
2017-10-03
*
Add decidable equality with nil
Jason Gross
2017-08-13
*
Make some tactics a bit more powerful
Jason Gross
2017-07-08
*
More fine-grained tactics imports
Jason Gross
2017-07-08
*
More fine-grained imports
Jason Gross
2017-07-08
*
Add UnfoldArg
Jason Gross
2017-07-08
*
prove an admit in ArithmeticSynthesisTest
Andres Erbsen
2017-07-06
*
Add wrappers for subborrow and add_with_get_carry so they work when it is not...
jadep
2017-06-29
*
remove unused admit (has been moved to Tuple.v)
jadep
2017-06-26
*
Prove map2_append
Jason Gross
2017-06-25
*
write and prove Tuple.map2_cps
jadep
2017-06-25
*
Fix a typo in push_Zmod that was causing looping
Jason Gross
2017-06-22
*
Fix some minor naming bugs in sig_assoc tactics
Jason Gross
2017-06-22
*
src/Demo.v: a 200-line introduction to BaseSystem ideas
Andres Erbsen
2017-06-21
*
Prove In_to_list_left_tl, In_left_hd, to_list_left_append
Jason Gross
2017-06-21
*
Add is_bounded_by_None_repeat_In_iff_lt
Jason Gross
2017-06-20
*
Add fold_left_orb_true, fold_left_orb_pull
Jason Gross
2017-06-20
*
Add is_bounded_by_None_repeat_In_iff
Jason Gross
2017-06-20
*
[Require NatUtil] should not change [tauto]
Jason Gross
2017-06-19
*
Add ModInv
Jason Gross
2017-06-18
*
Stronger zero_bounds
Jason Gross
2017-06-18
*
Add div_nonneg to zarith
Jason Gross
2017-06-18
*
Add Z.div_nonneg
Jason Gross
2017-06-18
*
Add eq_ZToWord
Jason Gross
2017-06-17
*
Unfold Z.mul_split_at_bitwidth for reification
Jason Gross
2017-06-17
*
finish tuple-ifying Montgomery API
jadep
2017-06-16
[next]