aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
* Add some equality lemmas about Positive{Map,Set}Gravatar Jason Gross2018-10-23
* Tactic-in-term: ensuring same scope for all occurrences of a notation variable.Gravatar Hugo Herbelin2018-10-23
* Add some zrange lemmasGravatar Jason Gross2018-10-11
* Export more tactics in Tactics.vGravatar Jason Gross2018-10-10
* Rename [normalize_commutative_identifier] file to match tactic nameGravatar Jason Gross2018-10-10
* Add [normalize_commutative_identifier] tacticGravatar Jason Gross2018-10-10
* Add some natutil and listutil lemmasGravatar Jason Gross2018-10-10
* Add map_update_nth_extGravatar Jason Gross2018-10-09
* Add ListUtil.ForallInGravatar Jason Gross2018-10-09
* Fix and prove bounds for fancymachine operationsGravatar jadep2018-09-28
* Add some option bind lemmasGravatar Jason Gross2018-09-27
* Add more reflect tacticsGravatar Jason Gross2018-09-27
* Add some lemmas about Bool.reflectGravatar Jason Gross2018-09-27
* Add destruct_head_{False,Empty_set}Gravatar Jason Gross2018-09-27
* Add some Proper lemmas for Option.bindGravatar Jason Gross2018-09-27
* Export notations when importing primitiveGravatar Jason Gross2018-09-18
* Actually fix the build for Coq 8.7Gravatar Jason Gross2018-09-17
* Fix 8.7 buildGravatar Jason Gross2018-09-15
* Add nth_error_Proper_eqlistAGravatar Jason Gross2018-09-14
* Add list_elementwise_eqlistAGravatar Jason Gross2018-09-14
* Add PrimitiveSigmaGravatar Jason Gross2018-09-14
* Add option_beq argumentsGravatar Jason Gross2018-09-13
* Add option_beqGravatar Jason Gross2018-09-13
* Add a rudimentary arg parse moduleGravatar Jason Gross2018-08-30
* Do less reduction in split_in_contextGravatar Jason Gross2018-08-29
* Improve speed of do_with_exactly_one_hyp tacticGravatar Jason Gross2018-08-29
* Add src/Util/PER.vGravatar Jason Gross2018-08-29
* Add do_with_exactly_one_hypGravatar Jason Gross2018-08-29
* Minor improvements to various ZUtil things; boundsGravatar Jason Gross2018-08-25
* Minor rshi tweaksGravatar Jason Gross2018-08-24
* Add some cc_m morphismsGravatar Jason Gross2018-08-24
* Add Z.rshi_correct_fullGravatar Jason Gross2018-08-24
* Add Z.cc_m_eq_fullGravatar Jason Gross2018-08-24
* Add some basic ZRange lemmasGravatar Jason Gross2018-08-24
* Add ZRange.union_commGravatar Jason Gross2018-08-24
* Add a few more zsimplify_const lemmas about shiftGravatar Jason Gross2018-08-24
* Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtilGravatar Jason Gross2018-08-23
* Fix bounds on n_corners_and_zeroGravatar Jason Gross2018-08-16
* Prove monotonicity properties about zrangeGravatar Jason Gross2018-08-15
* Add more zutil morphismsGravatar Jason Gross2018-08-13
* Fix some bounds analysisGravatar Jason Gross2018-08-13
* Add some Z.le Proper hints to zarithGravatar Jason Gross2018-08-13
* Fix previous commitGravatar Jason Gross2018-08-13
* Move a lemmaGravatar Jason Gross2018-08-13
* Add the file proving split_bounds correctGravatar Jason Gross2018-08-13
* Fix split_bounds, prove it correctGravatar Jason Gross2018-08-13
* Factor through is_tighter_than_bool, add is_bounded_by_bool_Proper_if_sumbool...Gravatar Jason Gross2018-08-13
* Add some util lemmasGravatar Jason Gross2018-08-13
* Add ListUtil.map_nth_default_seqGravatar Jason Gross2018-08-10
* Make Prod.eta_expand also work in the contextGravatar Jason Gross2018-08-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 22:04:08 +0000