aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
* 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
* Reserve λ notationGravatar Jason Gross2016-09-02
* Add reserved syntax-let notationGravatar Jason Gross2016-09-02
* Don't zeta-reduce in [simplify_projections]Gravatar Jason Gross2016-09-02
* Add prod_beqGravatar Jason Gross2016-09-02
* Strip <infomsg>; it messes things up in Coq 8.6 displayGravatar Jason Gross2016-09-02
* Slightly better cfailGravatar Jason Gross2016-09-02
* Add cfail{2,3}Gravatar Jason Gross2016-09-02
* Add [idtac_goal]Gravatar Jason Gross2016-09-02
* Add constr-based idtac tacticsGravatar Jason Gross2016-09-02
* Add another reserved notationGravatar Jason Gross2016-09-01
* Add more reserved infixesGravatar Jason Gross2016-08-31
* Rename congrunce_option to inversion_option, add [inversion_prod]Gravatar Jason Gross2016-08-31
* Add congruence_option tacticGravatar Jason Gross2016-08-31
* Removed lingering SearchAbout.Gravatar jadep2016-08-31
* Defined an equality comparison for tuples that uses bool instead of Prop (lik...Gravatar jadep2016-08-31
* Integrate suggestions from AndresGravatar Jason Gross2016-08-25
* More zarithGravatar Jason Gross2016-08-24
* Add more reserved notationsGravatar Jason Gross2016-08-24
* Fewer side-conditions on zsimplifyGravatar Jason Gross2016-08-24
* Added rewrite hints for two ListUtil lemmasGravatar jadep2016-08-24
* Moved a tactic to Util/Tactics.vGravatar jadep2016-08-24
* Fix a typoGravatar Jason Gross2016-08-24
* Add map_cons from Coq 8.6Gravatar Jason Gross2016-08-24
* Merge branch 'fast-inverse'Gravatar jadep2016-08-24
|\
* | Fix a Hint Resolve typoGravatar Jason Gross2016-08-23
* | More ZUtilGravatar Jason Gross2016-08-23
* | More ZUtilGravatar Jason Gross2016-08-23
| * Updated AdditionChainExponentiation.v such that the exponentiation correctnes...Gravatar jadep2016-08-23
|/
* Merge.Gravatar jadep2016-08-21
|\
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-21 14:19:13 +0000