aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/Named
Commit message (Expand)AuthorAge
* Finish proof of wf_map_castGravatar Jason Gross2017-03-28
* Do more subst in ContextProperties/TacticsGravatar Jason Gross2017-03-28
* Add find_Name_and_val_SmartFlatTypeMapUnInterp2_Some_SomeGravatar Jason Gross2017-03-28
* Add aborted CompilePropertiesGravatar Jason Gross2017-03-22
* Add split_onames_split_namesGravatar Jason Gross2017-03-22
* Add length_fst_split_names_None_iffGravatar Jason Gross2017-03-22
* Add length_fst_split_names_Some_iffGravatar Jason Gross2017-03-22
* Prove that mapf_cast gives the correct boundsGravatar Jason Gross2017-03-22
* Add more to CompileWfGravatar Jason Gross2017-03-19
* Add MapCastWfGravatar 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
* 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
* 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
* Switch to fully uncurried form for reflectionGravatar Jason Gross2017-03-01
* Split off some bits of Reflection.SyntaxGravatar Jason Gross2017-01-26
* Remove the Const constructor of exprfGravatar Jason Gross2017-01-19
* Work around bug #5175 in 8.6Gravatar Jason Gross2016-11-01
* Add [f] to things that use [exprf] or [flat_type]Gravatar Jason Gross2016-10-31
* Add interp_type_gen_rel_pointwise2, *_gen => *Gravatar Jason Gross2016-10-28
* Make use of named syntax, do reg assign for fancyGravatar Jason Gross2016-09-22
* Add dead code eliminationGravatar Jason Gross2016-09-22
* Add a non-higher-order syntax, and reg assignmentGravatar Jason Gross2016-09-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 15:40:56 +0000