aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection
Commit message (Expand)AuthorAge
* Fix a name clashGravatar Jason Gross2017-03-14
* Add split_{m,o,}names_firstn_skipn and co.Gravatar Jason Gross2017-03-14
* Add NameUtilPropertiesGravatar Jason Gross2017-03-14
* Add InterpretToPHOASInterpGravatar Jason Gross2017-03-14
* Add Wf_InterpToPHOASGravatar Jason Gross2017-03-14
* Remove useless hypsGravatar Jason Gross2017-03-14
* Add InterpretToPHOASGravatar Jason Gross2017-03-14
* Move find_if_eq to Decidable.v, use Decidable in NamedGravatar Jason Gross2017-03-14
* Add ContextPropertiesGravatar Jason Gross2017-03-14
* Remove useless importsGravatar Jason Gross2017-03-14
* Move ContextOk to ContextDefinitionsGravatar Jason Gross2017-03-14
* Add lemma about wff and interpf of NamedGravatar Jason Gross2017-03-14
* Fix more unfoldingGravatar Jason Gross2017-03-10
* Fix more unfolding that shouldn't happenGravatar Jason Gross2017-03-10
* Make sure interp_flat_type isn't unfolded in SmartMapGravatar Jason Gross2017-03-10
* Add better SmartFlatTypeMapInterp2Gravatar Jason Gross2017-03-08
* Remove interp_genf from Named/SyntaxGravatar Jason Gross2017-03-08
* Remove stuff from Reflection/Named/SyntaxGravatar Jason Gross2017-03-08
* Add FMapContext, PositiveContextGravatar Jason Gross2017-03-08
* make 8.5 happyGravatar Andres Erbsen2017-03-02
* 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
* Add interp_flat_type_rel_pointwise_SmartVarfMap, interp_flat_type_rel_pointwi...Gravatar Jason Gross2017-02-28
* Add SmartVarfMap Proper instanceGravatar Jason Gross2017-02-28
* Deduplicate codeGravatar Jason Gross2017-02-28
* Add BoundsInterpretationsGravatar Jason Gross2017-02-23
* Minor change to reflection namingGravatar Jason Gross2017-02-23
* Add various reflection improvements, boundbycastGravatar Jason Gross2017-02-21
* Add interpf_smart_bound without exprfGravatar Jason Gross2017-02-21
* Rename Interp lemmasGravatar Jason Gross2017-02-21
* Add non-exprf version of interpf_smart_unboundGravatar Jason Gross2017-02-16
* Add MapCastInterpGravatar Jason Gross2017-02-16
* Add InterpByIsoProofsGravatar Jason Gross2017-02-16
* Fix typoGravatar Jason Gross2017-02-16
* Add InterpByIsoGravatar Jason Gross2017-02-16
* Add rudimentary Java and C notation files, displayGravatar Jason Gross2017-02-15
* Remove useless commentGravatar Jason Gross2017-02-14
* Mostly finish Wf_BoundifyGravatar Jason Gross2017-02-14
* Prove wff_bound_opGravatar Jason Gross2017-02-14
* Stub for wff_bound_opGravatar Jason Gross2017-02-14
* Add Wf_MapInterpCast to wf databaseGravatar Jason Gross2017-02-14
* A bit more progress on BoundByCastWfGravatar Jason Gross2017-02-14
* Add partially finished MapCastWfGravatar Jason Gross2017-02-14
* Add src/Reflection/BoundByCastWf.vGravatar Jason Gross2017-02-14
* Update assumptions in src/Reflection/SmartBoundWf.vGravatar Jason Gross2017-02-14
* Add SmartBoundWfGravatar Jason Gross2017-02-14
* Prove nicer version of wf_SmartAbsGravatar Jason Gross2017-02-13
* Add partially admitted lemma wf_SmartAbsGravatar Jason Gross2017-02-13
* More uniform namingGravatar Jason Gross2017-02-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 13:10:14 +0000