aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
...
* Add more Forall2 lemmasGravatar Jason Gross2018-12-04
* Add more ListUtil Forall LemmasGravatar Jason Gross2018-12-04
* Add some ListUtil lemmas about Forall2Gravatar Jason Gross2018-12-04
* Remove ListUtil.List.repeatGravatar Jason Gross2018-12-04
* Revert "Add inversion_clear tactics"Gravatar Jason Gross2018-12-04
* Add inversion_clear tacticsGravatar Jason Gross2018-12-04
* Global Set Fast Name PrintingGravatar Jason Gross2018-11-27
* Add related_sigT_by_eq proper lemmasGravatar Jason Gross2018-11-19
* Add more reserved notationsGravatar Jason Gross2018-11-19
* Add related_sigT_by_eqGravatar Jason Gross2018-11-16
* Add map_repeat, map_constGravatar Jason Gross2018-11-11
* Add a variant of cps_id that pulls the continuation from the lhsGravatar Jason Gross2018-11-08
* Add some zrange lemmasGravatar Jason Gross2018-11-01
* Make pairs work in Z_cast2Gravatar Jason Gross2018-11-01
* Export ZRange operation notationsGravatar Jason Gross2018-11-01
* Add zrange notationsGravatar Jason Gross2018-11-01
* Add more reserved notationsGravatar Jason Gross2018-11-01
* Add more zrange operationsGravatar Jason Gross2018-11-01
* Tactic-in-term: ensuring same scope for all occurrences of a notation variable.Gravatar Hugo Herbelin2018-11-01
* Add PositiveSet FactsGravatar Jason Gross2018-10-29
* Add eqlistA_eq_iffGravatar Jason Gross2018-10-29
* Add split_contravariant_orGravatar Jason Gross2018-10-29
* Add ex_eq_and tacticGravatar Jason Gross2018-10-29
* Add some lemmas about ex, and, eqGravatar Jason Gross2018-10-29
* Improve cps_id tactics, add add_var_types_cps_id, unify_extracted_cps_id tacticsGravatar Jason Gross2018-10-28
* Fix a bug in ensure_complex_continuationGravatar Jason Gross2018-10-28
* Add CPSId tacticsGravatar Jason Gross2018-10-28
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-27 05:02:45 +0000