aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/WfProofs.v
Commit message (Expand)AuthorAge
* Adjust implicits of flatten_binding_list_same_in_eqGravatar Jason Gross2017-03-01
* Add flatten_binding_list_In_eq_iff, flatten_binding_list_same_in_eqGravatar Jason Gross2017-03-01
* Switch to fully uncurried form for reflectionGravatar Jason Gross2017-03-01
* Prove nicer version of wf_SmartAbsGravatar Jason Gross2017-02-13
* Add partially admitted lemma wf_SmartAbsGravatar Jason Gross2017-02-13
* Add wf databaseGravatar Jason Gross2017-02-01
* Add wff_SmartVarVarf_nilGravatar Jason Gross2017-02-01
* Add In_G_wff_SmartVarf, SmartVarf_PairGravatar Jason Gross2017-01-30
* Split off some bits of Reflection.SyntaxGravatar Jason Gross2017-01-26
* Add flatten_binding_list2_SmartVarfMap{1,2}Gravatar Jason Gross2017-01-25
* Lemmas about flatten_binding_list2Gravatar Jason Gross2017-01-25
* Generalize flatten_binding_list_SmartValfGravatar Jason Gross2017-01-24
* Add flatten_binding_list_SmartValfGravatar Jason Gross2017-01-24
* Add flatten_binding_list_SmartVarfMapGravatar Jason Gross2017-01-24
* Remove the Const constructor of exprfGravatar Jason Gross2017-01-19
* Move things to ExprInversionGravatar Jason Gross2016-12-03
* Add [f] to things that use [exprf] or [flat_type]Gravatar Jason Gross2016-10-31
* Add more WfProofsGravatar Jason Gross2016-10-29
* Add interp_type_gen_rel_pointwise2, *_gen => *Gravatar Jason Gross2016-10-28
* Split off lemmas about [InlineConst]Gravatar Jason Gross2016-09-16
* Reorder WfProofs argumentsGravatar Jason Gross2016-09-05
* Fix order of binders, and add WfProofsGravatar Jason Gross2016-09-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-08 08:48:51 +0000