aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
...
* Finish and enable rule-specific rewriter wf proofsGravatar Jason Gross2018-08-13
* 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
* Prove rewrite-rule-independent parts of rewrite WfGravatar Jason Gross2018-08-13
* Don't guarantee anything about casting outside of rangeGravatar Jason Gross2018-08-10
* Add related_hetero_iff_app_curriedGravatar Jason Gross2018-08-10
* Add ListUtil.map_nth_default_seqGravatar Jason Gross2018-08-10
* Make Prod.eta_expand also work in the contextGravatar Jason Gross2018-08-10
* Better transport lemmas in LanguageInversionGravatar Jason Gross2018-08-09
* Add ListUtil.{combine_repeat,combine_rev_rev_samelength}Gravatar Jason Gross2018-08-09
* Improve the power of split_andbGravatar Jason Gross2018-08-09
* Don't fuse annotationsGravatar Jason Gross2018-08-09
* Add more interp lemmasGravatar Jason Gross2018-08-09
* Push back admits in interp lemmasGravatar Jason Gross2018-08-08
* Add Wf_of_Wf3Gravatar Jason Gross2018-08-08
* Reserve 'n notation in Notations.vGravatar Jason Gross2018-08-08
* Add some partial interp proofs for abs-intGravatar Jason Gross2018-08-08
* Add lemmas about type.and_for_each_lhs_of_arrowGravatar Jason Gross2018-08-07
* Finish relax interp proofsGravatar Jason Gross2018-08-07
* Add another GeneralizeVar pass to add support for using Wf3Gravatar Jason Gross2018-08-07
* Fix an issue with the previous commitGravatar Jason Gross2018-08-07
* Add Proof using to arithmetic proofsGravatar Jason Gross2018-08-07
* Add type.related_hetero3Gravatar Jason Gross2018-08-06
* Start setting up abs-int interp proofsGravatar Jason Gross2018-08-06
* Add gen_interp_ProperGravatar Jason Gross2018-08-06
* Add app_curried_Proper_gen as an instanceGravatar Jason Gross2018-08-06
* Add related_iff_app_curriedGravatar Jason Gross2018-08-06
* Remove fastpath for Zcast in absintGravatar Jason Gross2018-08-06
* Remove thunking from abstract interpretationGravatar Jason Gross2018-08-06
* Generalize interp flat lemmasGravatar Jason Gross2018-08-06
* Generalize wf_interp_ProperGravatar Jason Gross2018-08-06
* Finish AbsInt Wf proofsGravatar Jason Gross2018-08-04
* Backwards compatible fix for some issues from https://github.com/coq/coq/pull...Gravatar Jason Gross2018-08-04
* Add wf for DefaultValueGravatar Jason Gross2018-08-03
* Add wf_splice_list, wf_splice_list_no_orderGravatar Jason Gross2018-08-03
* Fix typo in previous commitGravatar Jason Gross2018-08-03
* Add eq_ident_DecidableGravatar Jason Gross2018-08-03
* Add reflect_list_cps_idGravatar Jason Gross2018-08-03
* Better rewrite_type_transport_correctGravatar Jason Gross2018-08-02
* Adjust GENERATEDIdentifiersWithoutTypesProofs.v, add eta_ident_cps_correctGravatar Jason Gross2018-08-02
* Add GENERATEDIdentifiersWithoutTypesProofs.vGravatar Jason Gross2018-08-02
* Also generate decidable equality for pattern.identGravatar Jason Gross2018-08-02
* Make wf_safe_t a bit strongerGravatar Jason Gross2018-08-02
* Make ERROR_BAD_REWRITE_RULE Opaque, not Qed'edGravatar Jason Gross2018-08-02
* Generalize option_eq to support heterogenous relationsGravatar Jason Gross2018-08-02
* Add nth_error_combineGravatar Jason Gross2018-08-01
* More precise wf_Proper_list_implGravatar Jason Gross2018-07-31
* Comment out wf_splice_listGravatar Jason Gross2018-07-31
* Add wf_Proper_list, wf_splice_listGravatar Jason Gross2018-07-31
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-12 00:57:06 +0000