aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v
Commit message (Expand)AuthorAge
* move src/Experiments/NewPipeline/ to src/Gravatar Andres Erbsen2019-01-09
* remove pattern.ident.type_varsGravatar Jason Gross2018-12-11
* Prove pattern.ident.type_vars_enoughGravatar Jason Gross2018-12-08
* Restore Redirect in comment blocksGravatar Jason Gross2018-10-09
* Remove [Redirect] to absolute pathsGravatar Andres Erbsen2018-10-09
* Add pattern.ident.to_typedGravatar Jason Gross2018-10-01
* Support type variables in patterns in the rewriterGravatar Jason Gross2018-09-29
* Also generate decidable equality for pattern.identGravatar Jason Gross2018-08-02
* 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
* WIPGravatar Jason Gross2018-07-03
* New pipeline, split among filesGravatar Jason Gross2018-06-17