aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/NewPipeline/Language.v
Commit message (Expand)AuthorAge
* Help for fixpoint refolding in expr.interpGravatar Jason Gross2018-09-11
* Add andb_each_lhs_of_arrowGravatar Jason Gross2018-08-16
* Add type.related_hetero3Gravatar Jason Gross2018-08-06
* Add type.related_heteroGravatar Jason Gross2018-07-30
* Generalize type.eqv a bitGravatar Jason Gross2018-07-30
* Integrate Wf and Interp proofsGravatar Jason Gross2018-07-30
* More proofs about wf / interpGravatar Jason Gross2018-07-27
* Add invert_nil, invert_consGravatar Jason Gross2018-07-27
* Set arguments of ident.{gen_,}interpGravatar Jason Gross2018-07-27
* Put == in type_scope, so that we don't need to go around opening etype_scopeGravatar Jason Gross2018-07-26
* Add type.eqv for interp equivalenceGravatar Jason Gross2018-07-26
* Add invert_LetInGravatar Jason Gross2018-07-25
* 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
* WIPGravatar Jason Gross2018-07-03
* Make all parameters implicitGravatar Jasper Hugunin2018-07-02
* Remove useless RequiresGravatar Jason Gross2018-06-28
* New pipeline, split among filesGravatar Jason Gross2018-06-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-21 10:37:40 +0000