aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Minor additionsGravatar Jason Gross2017-01-23
* Fix a typoGravatar Jason Gross2017-01-23
* Add invert_expr_substGravatar Jason Gross2017-01-23
* Allow inversion on wff if either side is not a varGravatar Jason Gross2017-01-23
* Don't remake .v.d. files in clean-coqprimeGravatar Jason Gross2017-01-22
* Update _CoqProjectGravatar Jason Gross2017-01-21
* Add transparent equality proofs for fixed wordTGravatar Jason Gross2017-01-21
* Revert "Fix a missing qualification"Gravatar Jason Gross2017-01-21
* Fix a missing qualificationGravatar Jason Gross2017-01-21
* Move weqb_hetero to Bedrock.WordGravatar Jason Gross2017-01-21
* Add weqb_heteroGravatar Jason Gross2017-01-21
* Add split_andb tacticGravatar Jason Gross2017-01-21
* Add LetInMonad to _CoqProjectGravatar Jason Gross2017-01-19
* Update notations from zetabaseGravatar Jason Gross2017-01-19
* Add ZUtil lemma from zetabaseGravatar Jason Gross2017-01-19
* Remove the Const constructor of exprfGravatar Jason Gross2017-01-19
* Make f_equal2 transparent in equality proofGravatar Jason Gross2017-01-19
* Add nat_beq_to_eqGravatar Jason Gross2017-01-19
* Split out Reflection.Equality, change Tflat implicit argumentGravatar Jason Gross2017-01-19
* Fix infinite loop in destruct_rewrite_sumboolGravatar Jason Gross2017-01-17
* Fix changed qualified tactic nameGravatar Jason Gross2017-01-17
* More fine-grained util tactic filesGravatar Jason Gross2017-01-17
* Add document describing suggested cleanupGravatar jadep2017-01-17
* Use match in curry2; this gives better reificationGravatar Jason Gross2017-01-15
* Add curry.vGravatar Jason Gross2017-01-15
* More universe fixesGravatar Jason Gross2017-01-15
* Fix an issue with universesGravatar Jason Gross2017-01-15
* Update expansion.mdGravatar Andres Erbsen2017-01-13
* Add link to CEP in expansion.mdGravatar Jason Gross2017-01-12
* list of possible expansionsGravatar Andres Erbsen2017-01-12
* record golang poly1305 bugGravatar Andres Erbsen2017-01-11
* Add ApplicationRelationsGravatar Jason Gross2017-01-10
* another update to optimizations.mdGravatar jadep2017-01-09
* optimizations.md: recategorize + reorderGravatar jadep2017-01-09
* Add Syntax.tuple_mapGravatar Jason Gross2017-01-09
* optimizations.md: recategorize a couple thingsGravatar jadep2017-01-09
* Add >>> reserved notationGravatar Jason Gross2017-01-09
* Add Zmod_to_equiv_moduloGravatar Jason Gross2017-01-09
* optimizations.md: add missing descriptions and Karatsuba's trickGravatar jadep2017-01-09
* optimizations.md: formatting fixGravatar jadep2017-01-09
* optimizations.md: formatting fixGravatar jadep2017-01-09
* optimizations.md: formatting fixGravatar jadep2017-01-09
* Add descriptions to optimizations.mdGravatar jadep2017-01-09
* fix typo in optimizations.mdGravatar jadep2017-01-09
* shorten links in optimizations.mdGravatar jadep2017-01-09
* Add list of optimizations currently implementedGravatar jadep2017-01-09
* Update list of .PHONY targetsGravatar Jason Gross2017-01-09
* update-_CoqProjectGravatar Jason Gross2017-01-07
* copy_boundsGravatar Jason Gross2017-01-07
* Add reified LadderStep without carriesGravatar Jason Gross2017-01-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-31 12:28:00 +0000