aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection
Commit message (Expand)AuthorAge
* Add wf databaseGravatar Jason Gross2017-02-01
* Generalize InlineInterpGravatar Jason Gross2017-02-01
* Fix lazymatch orderingGravatar Jason Gross2017-02-01
* More powerful preinvert_one_typeGravatar Jason Gross2017-02-01
* Add invert_match_opGravatar Jason Gross2017-02-01
* Add invert_opGravatar Jason Gross2017-02-01
* Add inversion_exprGravatar Jason Gross2017-02-01
* Add invert_match_exprGravatar Jason Gross2017-02-01
* Add invert_exprGravatar Jason Gross2017-02-01
* Add wff_SmartVarVarf_nilGravatar Jason Gross2017-02-01
* Preferentially invert wff with two constructorsGravatar Jason Gross2017-01-31
* Nicer inversion_wffGravatar Jason Gross2017-01-31
* Fix implicitsGravatar Jason Gross2017-01-31
* Add SmartFlatTypeMap2Interp2Gravatar Jason Gross2017-01-31
* Add inversion_flat_type, inversion_typeGravatar Jason Gross2017-01-30
* Add In_G_wff_SmartVarf, SmartVarf_PairGravatar Jason Gross2017-01-30
* Add interp_flat_type_rel_pointwise0Gravatar Jason Gross2017-01-27
* Better typing for SmartPairf_PairGravatar Jason Gross2017-01-27
* Remove dead codeGravatar Jason Gross2017-01-27
* Add SmartPairf_PairGravatar Jason Gross2017-01-27
* Doc fixupGravatar Jason Gross2017-01-27
* Various minor reflection fixupsGravatar Jason Gross2017-01-27
* Split off some bits of Reflection.SyntaxGravatar Jason Gross2017-01-26
* Add interp_type_rel_pointwise2_heteroGravatar Jason Gross2017-01-25
* Add interp_flat_type_rel_pointwise2_hetero_flatten_binding_list2Gravatar Jason Gross2017-01-25
* Add flatten_binding_list2_SmartVarfMap{1,2}Gravatar Jason Gross2017-01-25
* Lemmas about flatten_binding_list2Gravatar Jason Gross2017-01-25
* Add flatten_binding_list2Gravatar Jason Gross2017-01-25
* Add interp_flat_type_rel_pointwise2_heteroGravatar Jason Gross2017-01-25
* Generalize flatten_binding_list_SmartValfGravatar Jason Gross2017-01-24
* Add flatten_binding_list_SmartValfGravatar Jason Gross2017-01-24
* Add SmartFlatTypeUnMapGravatar Jason Gross2017-01-24
* Add flatten_binding_list_SmartVarfMapGravatar Jason Gross2017-01-24
* Add SmartVarf{Type,Prop}Map{,2}Gravatar Jason Gross2017-01-24
* Add SmartVarfMap_idGravatar Jason Gross2017-01-24
* Add SmartVarfMap2Gravatar Jason Gross2017-01-24
* Add smart_interp_flat_map2Gravatar Jason Gross2017-01-24
* Preserve names in invert_expr_substGravatar Jason Gross2017-01-23
* Make invert_expr_subst not loopGravatar Jason Gross2017-01-23
* Fix invert_expr_substGravatar Jason Gross2017-01-23
* Better invert_exprGravatar Jason Gross2017-01-23
* Minor additionsGravatar Jason Gross2017-01-23
* Fix a typoGravatar Jason Gross2017-01-23
* Add invert_expr_substGravatar Jason Gross2017-01-23
* Allow inversion on wff if either side is not a varGravatar Jason Gross2017-01-23
* Remove the Const constructor of exprfGravatar Jason Gross2017-01-19
* Make f_equal2 transparent in equality proofGravatar Jason Gross2017-01-19
* Split out Reflection.Equality, change Tflat implicit argumentGravatar Jason Gross2017-01-19
* More fine-grained util tactic filesGravatar Jason Gross2017-01-17
* Add ApplicationRelationsGravatar Jason Gross2017-01-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-15 23:37:25 +0000