aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/NewPipeline/RewriterWf2.v
Commit message (Expand)AuthorAge
* move src/Experiments/NewPipeline/ to src/Gravatar Andres Erbsen2019-01-09
* Fix a bug in 0672c92921e45b942fa8a75c45457b8c7b32565dGravatar Jason Gross2018-12-12
* remove pattern.ident.type_varsGravatar Jason Gross2018-12-11
* Switch to a more precise version of interp_related for rewritesGravatar Jason Gross2018-12-07
* Fix bug in previous commitGravatar Jason Gross2018-11-16
* Uncurry rewriter rulesGravatar Jason Gross2018-11-15
* Add under_forall_vars_relation1_lam_forall_vars, remove forall2_type_of_list_...Gravatar Jason Gross2018-10-25
* Minor changes to rewriterGravatar Jason Gross2018-10-14
* Add interp-correctness condition for rewriterGravatar Jason Gross2018-10-11
* 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
* Finish rule-specific rewriter wf proofsGravatar Jason Gross2018-08-13
* Improvements in rewrite-rule-specific proofsGravatar Jason Gross2018-08-13
* Split up rewrite rules proofs into multiple filesGravatar Jason Gross2018-08-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-21 16:33:06 +0000