aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection
Commit message (Expand)AuthorAge
* Also count lets in operations and pairsGravatar Jason Gross2017-03-22
* Add length_fst_split_names_Some_iffGravatar Jason Gross2017-03-22
* Fix MapCastByDeBruijnInterpGravatar Jason Gross2017-03-22
* Prove that mapf_cast gives the correct boundsGravatar Jason Gross2017-03-22
* Add debug output for success in reifyfGravatar Jason Gross2017-03-22
* Add cast_back_flat_constGravatar Jason Gross2017-03-22
* Make Z.ltb_to_lt a bit strongerGravatar Jason Gross2017-03-21
* Add aborted MapCastByDeBruijnWfGravatar Jason Gross2017-03-19
* Finish MapCastCorrectGravatar Jason Gross2017-03-19
* Add more to CompileWfGravatar Jason Gross2017-03-19
* Add MapCastWfGravatar Jason Gross2017-03-19
* Most of the way towards a complete MapCastCorrectGravatar Jason Gross2017-03-19
* Add Named/PositiveContext/DefaultsProperties.vGravatar Jason Gross2017-03-19
* Finish CompileInterp proofGravatar Jason Gross2017-03-19
* Split up ContextPropertiesGravatar Jason Gross2017-03-19
* Add mname_list_unique_nilGravatar Jason Gross2017-03-19
* Add more ContextPropertiesGravatar Jason Gross2017-03-19
* Add {m,o,}name_list_uniqueGravatar Jason Gross2017-03-19
* Add Addmitted correctness for MapCastByDeBruijnGravatar Jason Gross2017-03-19
* Add dummy TWord constructor to syntax typeGravatar Jason Gross2017-03-19
* Minor simplification in SmartBoundGravatar Jason Gross2017-03-18
* Switch to more robust automation in MapCastInterpGravatar Jason Gross2017-03-17
* Add default_names_for{,f}Gravatar Jason Gross2017-03-17
* Add IdContextGravatar Jason Gross2017-03-17
* Revert "Have cast_op return exprf instead of op"Gravatar Jason Gross2017-03-17
* Have cast_op return exprf instead of opGravatar Jason Gross2017-03-17
* Add MapCastByDeBruijn on PHOAS syntaxGravatar Jason Gross2017-03-17
* Don't pass a wf proof into InterpToPHOASGravatar Jason Gross2017-03-17
* Add aborted in-process compile-{wf,interp} proofsGravatar Jason Gross2017-03-17
* Add a Named version of MapCastGravatar Jason Gross2017-03-17
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 13:48:06 +0000