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
...
*
Add related_sigT_by_eq
Jason Gross
2018-11-16
*
Add map_repeat, map_const
Jason Gross
2018-11-11
*
Add a variant of cps_id that pulls the continuation from the lhs
Jason Gross
2018-11-08
*
Add some zrange lemmas
Jason Gross
2018-11-01
*
Make pairs work in Z_cast2
Jason Gross
2018-11-01
*
Export ZRange operation notations
Jason Gross
2018-11-01
*
Add zrange notations
Jason Gross
2018-11-01
*
Add more reserved notations
Jason Gross
2018-11-01
*
Add more zrange operations
Jason Gross
2018-11-01
*
Tactic-in-term: ensuring same scope for all occurrences of a notation variable.
Hugo Herbelin
2018-11-01
*
Add PositiveSet Facts
Jason Gross
2018-10-29
*
Add eqlistA_eq_iff
Jason Gross
2018-10-29
*
Add split_contravariant_or
Jason Gross
2018-10-29
*
Add ex_eq_and tactic
Jason Gross
2018-10-29
*
Add some lemmas about ex, and, eq
Jason Gross
2018-10-29
*
Improve cps_id tactics, add add_var_types_cps_id, unify_extracted_cps_id tactics
Jason Gross
2018-10-28
*
Fix a bug in ensure_complex_continuation
Jason Gross
2018-10-28
*
Add CPSId tactics
Jason Gross
2018-10-28
*
Add some equality lemmas about Positive{Map,Set}
Jason Gross
2018-10-23
*
Tactic-in-term: ensuring same scope for all occurrences of a notation variable.
Hugo Herbelin
2018-10-23
*
Add some zrange lemmas
Jason Gross
2018-10-11
*
Export more tactics in Tactics.v
Jason Gross
2018-10-10
*
Rename [normalize_commutative_identifier] file to match tactic name
Jason Gross
2018-10-10
*
Add [normalize_commutative_identifier] tactic
Jason Gross
2018-10-10
*
Add some natutil and listutil lemmas
Jason Gross
2018-10-10
*
Add map_update_nth_ext
Jason Gross
2018-10-09
*
Add ListUtil.ForallIn
Jason Gross
2018-10-09
*
Fix and prove bounds for fancymachine operations
jadep
2018-09-28
*
Add some option bind lemmas
Jason Gross
2018-09-27
*
Add more reflect tactics
Jason Gross
2018-09-27
*
Add some lemmas about Bool.reflect
Jason Gross
2018-09-27
*
Add destruct_head_{False,Empty_set}
Jason Gross
2018-09-27
*
Add some Proper lemmas for Option.bind
Jason Gross
2018-09-27
*
Export notations when importing primitive
Jason Gross
2018-09-18
*
Actually fix the build for Coq 8.7
Jason Gross
2018-09-17
*
Fix 8.7 build
Jason Gross
2018-09-15
*
Add nth_error_Proper_eqlistA
Jason Gross
2018-09-14
*
Add list_elementwise_eqlistA
Jason Gross
2018-09-14
*
Add PrimitiveSigma
Jason Gross
2018-09-14
*
Add option_beq arguments
Jason Gross
2018-09-13
*
Add option_beq
Jason Gross
2018-09-13
*
Add a rudimentary arg parse module
Jason Gross
2018-08-30
*
Do less reduction in split_in_context
Jason Gross
2018-08-29
*
Improve speed of do_with_exactly_one_hyp tactic
Jason Gross
2018-08-29
*
Add src/Util/PER.v
Jason Gross
2018-08-29
*
Add do_with_exactly_one_hyp
Jason Gross
2018-08-29
*
Minor improvements to various ZUtil things; bounds
Jason Gross
2018-08-25
*
Minor rshi tweaks
Jason Gross
2018-08-24
*
Add some cc_m morphisms
Jason Gross
2018-08-24
*
Add Z.rshi_correct_full
Jason Gross
2018-08-24
[prev]
[next]