aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/WfProofs.v
Commit message (Expand)AuthorAge
* Generalize In_flatten_binding_list_untransfer_interp_flat_typeGravatar Jason Gross2017-10-24
* Add In_flatten_binding_list_untransfer_interp_flat_typeGravatar Jason Gross2017-10-24
* Add wff_SmartPairf_SmartValfGravatar Jason Gross2017-10-24
* Add wff_SmartPairf_SmartVarfMap_sameGravatar Jason Gross2017-10-20
* Add wff_invert_PairsConstGravatar Jason Gross2017-10-20
* Prove flatten_binding_list_interpf_SmartPairf_sameGravatar Jason Gross2017-10-20
* Add wff_SmartPairfGravatar Jason Gross2017-10-20
* Add flatten_binding_list_SmartVarfMap2_pair_in_generalize2Gravatar Jason Gross2017-05-13
* Add flatten_binding_list_SmartVarfMap2_pair_In_splitGravatar Jason Gross2017-04-10
* Add flatten_binding_list_SmartVarfMap2_pair_same_in_eq2Gravatar Jason Gross2017-04-10
* rename-everythingGravatar Andres Erbsen2017-04-06