aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
* More zsimplify lemmasGravatar Jason Gross2016-10-04
* Add Zplus_minus to zsimplifyGravatar Jason Gross2016-10-04
* Weaken hyps of zutil lemmaGravatar Jason Gross2016-10-04
* Add a variant of add_shift_modGravatar Jason Gross2016-10-04
* Add ZUtil lemmaGravatar Jason Gross2016-10-04
* Add ZUtil lemmaGravatar Jason Gross2016-10-04
* Add Zmult_lt_compat_r to zarithGravatar Jason Gross2016-10-04
* Prevent infinite loops by not dealing with 0 mod _Gravatar Jason Gross2016-10-04
* Handle 0 mod _ in push_ZmodGravatar Jason Gross2016-10-04
* Handle ?x mod ?x in push_ZmodGravatar Jason Gross2016-10-04
* Z.ltb_to_lt now also handles eqbGravatar Jason Gross2016-10-04
* Work around bug 5107 (broken return inference)Gravatar Jason Gross2016-10-03
* Work around bug #5112 ([Arguments id /] broken)Gravatar Jason Gross2016-09-30
* Add Tuple.mapGravatar Jason Gross2016-09-29
* Revert "Add a locked version of [let] with fewer reductions"Gravatar Jason Gross2016-09-22
* Revert "Fix LockedLet"Gravatar Jason Gross2016-09-22
* Fix a typoGravatar Jason Gross2016-09-22
* Add a form of Let_In that carries a proofGravatar Jason Gross2016-09-22
* alternative signing derivationGravatar Andres Erbsen2016-09-22
* Util.LetIn: fix proper instanceGravatar Andres Erbsen2016-09-22
* Fix LockedLetGravatar Jason Gross2016-09-22
* Add a locked version of [let] with fewer reductionsGravatar Jason Gross2016-09-22
* Reorganization, moving of lemmas to correct files, and 8.4 compatibilityGravatar jadep2016-09-21
* Change [Let ... in ...] to [dlet ... in ...] (#67)Gravatar Jason Gross2016-09-19
* Add dec eq for option, listGravatar Jason Gross2016-09-18
* Util.Notations: change Let to match slet\Gravatar Andres Erbsen2016-09-18
* Add reserved notation for Let, change #Gravatar Jason Gross2016-09-17
* Move side lemmas to appropriate filesGravatar jadep2016-09-17
* deduplicate Let_In into src/Util/LetIn.vGravatar Andres Erbsen2016-09-17
* Add λn reserved notationGravatar Jason Gross2016-09-16
* Fix for Coq 8.5Gravatar Jason Gross2016-09-16
* Add more prop_of_optionGravatar Jason Gross2016-09-16
* Derive EdDSA.verify from equational specificationGravatar Andres Erbsen2016-09-16
* IterAssocOp: parameters before argumentsGravatar Andres Erbsen2016-09-16
* Equality for nat in natutilGravatar Jason Gross2016-09-16
* More 8.4 compatibilityGravatar jadep2016-09-14
* Moved lemmas to ZUtilGravatar jadep2016-09-13
* Fully qualify [Require]sGravatar Jason Gross2016-09-08
* Work around bug #5073 (lia)Gravatar Jason Gross2016-09-07
* Add nth_error_In from 8.6Gravatar Jason Gross2016-09-05
* Add connectives about option pointed_PropGravatar Jason Gross2016-09-05
* Add a coercion [bool >-> option pointed_Prop]Gravatar Jason Gross2016-09-05
* Fix a typoGravatar Jason Gross2016-09-05
* Add a file about pointed PropsGravatar Jason Gross2016-09-05
* Add a lemma about semidecidable things to DecidableGravatar Jason Gross2016-09-05
* Make [inversion_{prod,sigma}] strongerGravatar Jason Gross2016-09-05
* Transparent version of f_equal2Gravatar Jason Gross2016-09-05
* Reserve [->] like in 8.5, so we can redefine it in 8.4Gravatar Jason Gross2016-09-05
* Add path_prod_etaGravatar Jason Gross2016-09-03
* Make [inversion_option] work on Prop optionsGravatar Jason Gross2016-09-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 00:26:00 +0000