| Commit message (Expand) | Author | Age |
* | Add cast_back_flat_const | Jason Gross | 2017-03-22 |
* | Make Z.ltb_to_lt a bit stronger | Jason Gross | 2017-03-21 |
* | Add aborted MapCastByDeBruijnWf | Jason Gross | 2017-03-19 |
* | Finish MapCastCorrect | Jason Gross | 2017-03-19 |
* | Add more to CompileWf | Jason Gross | 2017-03-19 |
* | Add MapCastWf | Jason Gross | 2017-03-19 |
* | Most of the way towards a complete MapCastCorrect | Jason Gross | 2017-03-19 |
* | Add Named/PositiveContext/DefaultsProperties.v | Jason Gross | 2017-03-19 |
* | Finish CompileInterp proof | Jason Gross | 2017-03-19 |
* | Split up ContextProperties | Jason Gross | 2017-03-19 |
* | Add mname_list_unique_nil | Jason Gross | 2017-03-19 |
* | Add more ContextProperties | Jason Gross | 2017-03-19 |
* | Add {m,o,}name_list_unique | Jason Gross | 2017-03-19 |
* | Add Addmitted correctness for MapCastByDeBruijn | Jason Gross | 2017-03-19 |
* | Add dummy TWord constructor to syntax type | Jason Gross | 2017-03-19 |
* | Minor simplification in SmartBound | Jason Gross | 2017-03-18 |
* | Switch to more robust automation in MapCastInterp | Jason Gross | 2017-03-17 |
* | Add default_names_for{,f} | Jason Gross | 2017-03-17 |
* | Add IdContext | Jason Gross | 2017-03-17 |
* | Revert "Have cast_op return exprf instead of op" | Jason Gross | 2017-03-17 |
* | Have cast_op return exprf instead of op | Jason Gross | 2017-03-17 |
* | Add MapCastByDeBruijn on PHOAS syntax | Jason Gross | 2017-03-17 |
* | Don't pass a wf proof into InterpToPHOAS | Jason Gross | 2017-03-17 |
* | Add aborted in-process compile-{wf,interp} proofs | Jason Gross | 2017-03-17 |
* | Add a Named version of MapCast | Jason Gross | 2017-03-17 |
* | Fix a name clash | Jason Gross | 2017-03-14 |
* | Add split_{m,o,}names_firstn_skipn and co. | Jason Gross | 2017-03-14 |
* | Add NameUtilProperties | Jason Gross | 2017-03-14 |
* | Add InterpretToPHOASInterp | Jason Gross | 2017-03-14 |
* | Add Wf_InterpToPHOAS | Jason Gross | 2017-03-14 |
* | Remove useless hyps | Jason Gross | 2017-03-14 |
* | Add InterpretToPHOAS | Jason Gross | 2017-03-14 |
* | Move find_if_eq to Decidable.v, use Decidable in Named | Jason Gross | 2017-03-14 |
* | Add ContextProperties | Jason Gross | 2017-03-14 |
* | Remove useless imports | Jason Gross | 2017-03-14 |
* | Move ContextOk to ContextDefinitions | Jason Gross | 2017-03-14 |
* | Add lemma about wff and interpf of Named | Jason Gross | 2017-03-14 |
* | Fix more unfolding | Jason Gross | 2017-03-10 |
* | Fix more unfolding that shouldn't happen | Jason Gross | 2017-03-10 |
* | Make sure interp_flat_type isn't unfolded in SmartMap | Jason Gross | 2017-03-10 |
* | Add better SmartFlatTypeMapInterp2 | Jason Gross | 2017-03-08 |
* | Remove interp_genf from Named/Syntax | Jason Gross | 2017-03-08 |
* | Remove stuff from Reflection/Named/Syntax | Jason Gross | 2017-03-08 |
* | Add FMapContext, PositiveContext | Jason Gross | 2017-03-08 |
* | make 8.5 happy | Andres Erbsen | 2017-03-02 |
* | Adjust implicits of flatten_binding_list_same_in_eq | Jason Gross | 2017-03-01 |
* | Add flatten_binding_list_In_eq_iff, flatten_binding_list_same_in_eq | Jason Gross | 2017-03-01 |
* | Switch to fully uncurried form for reflection | Jason Gross | 2017-03-01 |
* | Add interp_flat_type_rel_pointwise_SmartVarfMap, interp_flat_type_rel_pointwi... | Jason Gross | 2017-02-28 |
* | Add SmartVarfMap Proper instance | Jason Gross | 2017-02-28 |