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
*
Add correctness in arithmetic for mulx, addcarryx, subborrowx
Jason Gross
2018-12-21
*
Add has_body tactic
Jason Gross
2018-12-21
*
Add eval_freeze_to_bytesmod to push_eval
Jason Gross
2018-12-21
*
Add length_encode_no_reduce to distr_length
Jason Gross
2018-12-21
*
Add `Proof using` directives in Arithmetic
Jason Gross
2018-12-21
*
Fix a few minor things in Arithmetic
Jason Gross
2018-12-21
*
remove unneeded lemma and do some micro-performance-optimization at one stick...
jadep
2018-12-21
*
remove proof duplication
jadep
2018-12-21
*
fix hints and [Proof using] statements so that proofs go through
jadep
2018-12-21
*
prove [small_sub_then_maybe_add]
jadep
2018-12-21
*
prove [eval_sub_then_maybe_add]
jadep
2018-12-21
*
fix hints and [Proof using] statements so that proofs go through
jadep
2018-12-21
*
prove [small_conditional_sub]
jadep
2018-12-21
*
prove [eval_conditional_sub]
jadep
2018-12-21
*
move weight proofs up above Positional so they can be used to prove eval_drop...
jadep
2018-12-21
*
modify a proof because in 8.7 [auto] doesn't solve the goal
jadep
2018-12-21
*
prove admit
jadep
2018-12-21
*
prove admit
jadep
2018-12-21
*
Add Wf_reify
Jason Gross
2018-12-20
*
Add Wf_APP, Interp_reify
Jason Gross
2018-12-20
*
Remove glue admits in Toplevel1
Jason Gross
2018-12-20
*
Update .travis.yml
Jason Gross
2018-12-20
*
Add uweight_partition_unique, move weight_1 to uweight_1, add Positional.eval...
Jason Gross
2018-12-20
*
Finish rewriter proofs modulo funext
Jason Gross
2018-12-19
*
Add eq_subst_types_pattern_collect_vars_empty_iff
Jason Gross
2018-12-18
*
Add rawexpr_types_ok
Jason Gross
2018-12-14
*
Fix an issue with setoid_rewrite being weaker before 8.9
Jason Gross
2018-12-14
*
Add reify_and_let_binds_base_interp_related
Jason Gross
2018-12-14
*
add interp_related_gen_of_wf
Jason Gross
2018-12-12
*
Remove useless assumptions
Jason Gross
2018-12-12
*
Generalize expr.interp_related
Jason Gross
2018-12-12
*
Move fancy rewrites after bounds analysis
Jason Gross
2018-12-12
*
Fix a bug in 0672c92921e45b942fa8a75c45457b8c7b32565d
Jason Gross
2018-12-12
*
Add type.eq_subst_types_pattern_collect_vars
Jason Gross
2018-12-12
*
Make unify_pattern' a bit stricter
Jason Gross
2018-12-12
*
Add projT1_app_with_unification_resultT
Jason Gross
2018-12-12
*
Add rawexpr_interp_related_Proper_rawexpr_equiv_rew_gen
Jason Gross
2018-12-12
*
Add ZRange.cc_m, ZRange.is_bounded_by_bool_cc_m
Jason Gross
2018-12-11
*
Add ZRange.is_bounded_by_bool_normalize_constant
Jason Gross
2018-12-11
*
Add ZRange.normalize_constant
Jason Gross
2018-12-11
*
Add ZRange.is_bounded_by_bool_constant
Jason Gross
2018-12-11
*
Add ZRange.OperationBounds
Jason Gross
2018-12-11
*
remove pattern.ident.type_vars
Jason Gross
2018-12-11
*
Use Fixpoint, not list_rect, for {app,lam}_forall_vars
Jason Gross
2018-12-11
*
Add In_elements_mem_iff
Jason Gross
2018-12-11
*
Add eqv_iff_eq_of_funext
Jason Gross
2018-12-11
*
Prove pattern.ident.type_vars_enough
Jason Gross
2018-12-08
*
Add more windows binaries
Jason Gross
2018-12-07
*
Add value_of_rawexpr_interp_related
Jason Gross
2018-12-07
*
Switch to a more precise version of interp_related for rewrites
Jason Gross
2018-12-07
[next]