aboutsummaryrefslogtreecommitdiff
path: root/src/Rewriter.v
Commit message (Expand)AuthorAge
* Clean up notations after bbv removalHEADmasterGravatar Benjamin Barenblat2019-04-26
* Do less reduction in GENERATEDIdentifiersWithoutTypesGravatar Jason Gross2019-04-24
* Replace the python script with Ltac codeGravatar Jason Gross2019-04-12
* Automate more of the rewriter, and factor out rule-specific thingsGravatar Jason Gross2019-04-11
* Automate more of the rewriter reification, proofGravatar Jason Gross2019-04-09
* Add UnderLets flat_map interp proofs,other changesGravatar Jason Gross2019-04-04
* Add Z.combine_at_bitwidthGravatar Jason Gross2019-04-02
* Factor out rewriter rulesGravatar Jason Gross2019-03-31
* Fix a non-terminated commentGravatar Jason Gross2019-03-31
* Add some comments based on CR requestsGravatar Jason Gross2019-03-31
* Finish reifying list lemmasGravatar Jason Gross2019-03-31
* Add constr_fail and constr_fail_withGravatar Jason Gross2019-03-31
* Get new Barrett proofs to generate Fancy code as beforeGravatar jadep2019-03-25
* Reify most rewrite rulesGravatar Jason Gross2019-03-07
* Fix unfolding of pattern.base.lookup_defaultGravatar Jason Gross2019-03-05
* Fix an issue with a proof from the previous commitGravatar Jason Gross2019-03-04
* Add support for reifying `zrange` and `option`Gravatar Jason Gross2019-02-18
* Insert casts before literals during bounds analysisGravatar Jason Gross2019-02-11
* Remove an unused argumentGravatar Jason Gross2019-02-01
* Uncps unify_extractedGravatar Jason Gross2019-02-01
* Constant-propogate 0+x and x+0 after boundsGravatar Jason Gross2019-01-16
* Add a rewrite rule to collapse constant castsGravatar Jason Gross2019-01-16
* move src/Experiments/NewPipeline/ to src/Gravatar Andres Erbsen2019-01-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-28 00:38:49 +0000