aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Expand)AuthorAge
* Don't include extraction .vo files in the all targetGravatar Jason Gross2019-04-11
* sed s'/RewriterProofs/RewriterAll/g'Gravatar Jason Gross2019-04-11
* Make a single tactic to build the rewriterGravatar Jason Gross2019-04-11
* Automate more of the rewriter, and factor out rule-specific thingsGravatar Jason Gross2019-04-11
* run make update-_CoqProjectGravatar jadep2019-04-03
* rename some thingsGravatar jadep2019-04-03
* update _CoqProject, fix indentations, and prune dependencies of new Arithmeti...Gravatar jadep2019-04-03
* Add Z.combine_at_bitwidthGravatar Jason Gross2019-04-02
* Factor out rewriter rulesGravatar Jason Gross2019-03-31
* Add constr_fail and constr_fail_withGravatar Jason Gross2019-03-31
* Remove GlobalTacticalsGravatar Jason Gross2019-03-08
* Add some gtacticsGravatar Jason Gross2019-03-08
* Make [reflect] a typeclass and add a bunch of lemmasGravatar Jason Gross2019-03-04
* Add better computation of carry chainGravatar Jason Gross2019-01-26
* Split up PushButtonSynthesis.vGravatar Jason Gross2019-01-18
* Rename Translation.vGravatar jadep2019-01-17
* separate toplevel2 into several files; fix up final barrett proofGravatar jadep2019-01-17
* Move StringMap into Strings/Gravatar Jason Gross2019-01-15
* Add StringMapGravatar Jason Gross2019-01-15
* Add String_as_OTGravatar Jason Gross2019-01-15
* Autocompute s and c in WBW MontgomeryGravatar Jason Gross2019-01-14
* remove old pipelineGravatar Andres Erbsen2019-01-09
* move src/Experiments/NewPipeline/ to src/Gravatar Andres Erbsen2019-01-09
* new pipeline: refactor glue, split into more filesGravatar Jason Gross2019-01-05
* Add has_body tacticGravatar Jason Gross2018-12-21
* Finish rewriter proofs modulo funextGravatar Jason Gross2018-12-19
* Add ZRange.OperationBoundsGravatar Jason Gross2018-12-11
* Add related_sigT_by_eqGravatar Jason Gross2018-11-16
* Add PositiveSet FactsGravatar Jason Gross2018-10-29
* Add some lemmas about ex, and, eqGravatar Jason Gross2018-10-29
* Add CPSId tacticsGravatar Jason Gross2018-10-28
* Add some equality lemmas about Positive{Map,Set}Gravatar Jason Gross2018-10-23
* Add interp-correctness condition for rewriterGravatar Jason Gross2018-10-11
* Rename [normalize_commutative_identifier] file to match tactic nameGravatar Jason Gross2018-10-10
* Add [normalize_commutative_identifier] tacticGravatar Jason Gross2018-10-10
* Add ListUtil.ForallInGravatar Jason Gross2018-10-09
* Add some lemmas about Bool.reflectGravatar Jason Gross2018-09-27
* Add list_elementwise_eqlistAGravatar Jason Gross2018-09-14
* Add PrimitiveSigmaGravatar Jason Gross2018-09-14
* Add a rudimentary arg parse moduleGravatar Jason Gross2018-08-30
* Add src/Util/PER.vGravatar Jason Gross2018-08-29
* Minor improvements to various ZUtil things; boundsGravatar Jason Gross2018-08-25
* Bump bbvGravatar Jason Gross2018-08-24
* Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtilGravatar Jason Gross2018-08-23
* Add more operation-specific proofsGravatar Jason Gross2018-08-21
* Add the file proving split_bounds correctGravatar Jason Gross2018-08-13
* Split up rewrite rules proofs into multiple filesGravatar Jason Gross2018-08-13
* Start setting up abs-int interp proofsGravatar Jason Gross2018-08-06
* Add related_iff_app_curriedGravatar Jason Gross2018-08-06
* Add GENERATEDIdentifiersWithoutTypesProofs.vGravatar Jason Gross2018-08-02