aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
* 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
|\
* | ListUtil.v : new proofs about sum_firstn for lists with nonnegative elementsGravatar jadep2016-08-21
| * Add Z.rewrite_mod_smallGravatar Jason Gross2016-08-19
| * More powerful Z.div_mod_to_quot_remGravatar Jason Gross2016-08-19
| * More ZUtilGravatar Jason Gross2016-08-18
| * Add ZUtilGravatar Jason Gross2016-08-18
| * Add a ZUtil hintGravatar Jason Gross2016-08-18
| * Add some ZUtil lemmas and hintsGravatar Jason Gross2016-08-18
| * Add versions of ZUtil lemmas without nonzero assumptionsGravatar Jason Gross2016-08-18
| * Add Z.opp_involutive to Zshift_to_powGravatar Jason Gross2016-08-18
| * Add a ZUtil hintGravatar Jason Gross2016-08-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 05:12:25 +0000