aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/NewPipeline/Rewriter.v
Commit message (Expand)AuthorAge
* Update the post-bounds rewrite rulesGravatar Jason Gross2018-11-11
* Split off all of the arithmetic rules that need bounds infoGravatar Jason Gross2018-11-11
* Also inline Z_cast thingsGravatar Jason Gross2018-11-01
* Remove dead codeGravatar Jason Gross2018-11-01
* Stricter check on types in the rewriterGravatar Jason Gross2018-10-29
* Add an extra check in the rewriterGravatar Jason Gross2018-10-28
* Update rewriter correctness conditionGravatar Jason Gross2018-10-23
* Add placeholder rewrite rules for rewriting after boundsGravatar Jason Gross2018-10-14
* Minor changes to rewriterGravatar Jason Gross2018-10-14
* Remove [Redirect] to absolute pathsGravatar Andres Erbsen2018-10-09
* Fix a bad rewrite ruleGravatar Jason Gross2018-10-09
* Add under_with_unification_resultT_relation_heteroGravatar Jason Gross2018-10-09
* Add pattern.ident.to_typedGravatar Jason Gross2018-10-01
* Add a few rewriter definitionsGravatar Jason Gross2018-10-01
* Support type variables in patterns in the rewriterGravatar Jason Gross2018-09-29
* Split out rewrite_with_rule as a separate definitionGravatar Jason Gross2018-09-17
* Make ERROR_BAD_REWRITE_RULE Opaque, not Qed'edGravatar Jason Gross2018-08-02
* Move the associator pass to the rewriterGravatar Jason Gross2018-07-26
* Improve rewriter speedGravatar Jason Gross2018-07-25
* Revert "Improve rewriter speed"Gravatar Jason Gross2018-07-24
* Improve rewriter speedGravatar Jason Gross2018-07-24
* Montgomery reduction in new pipelineGravatar Jason Gross2018-07-21
* Support reification of firstn, skipnGravatar Jason Gross2018-07-18
* Allow reification of nat_rect (fun _ => _ -> _)Gravatar Jason Gross2018-07-15
* Correctly reify match on prodGravatar Jason Gross2018-07-03
* Pull out *2 in square, don't turn *2 into <<1Gravatar Jason Gross2018-07-03
* WIPGravatar Jason Gross2018-07-03
* Remove useless RequiresGravatar Jason Gross2018-06-28
* Add another prime exampleGravatar Jason Gross2018-06-18
* New pipeline, split among filesGravatar Jason Gross2018-06-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-20 10:44:35 +0000