aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/Syntax.v
Commit message (Expand)AuthorAge
* 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
* Add flatten_binding_list2Gravatar Jason Gross2017-01-25
* Add SmartFlatTypeUnMapGravatar 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
* Remove the Const constructor of exprfGravatar Jason Gross2017-01-19
* Split out Reflection.Equality, change Tflat implicit argumentGravatar Jason Gross2017-01-19
* Add Syntax.tuple_mapGravatar Jason Gross2017-01-09
* Transparent versions of {flat_,}type_eq_decGravatar Jason Gross2017-01-01
* Add smart_interp_map_genGravatar Jason Gross2017-01-01
* Add SmartFlatTypeMap2Gravatar Jason Gross2016-12-26
* Add flatten_flat_typeGravatar Jason Gross2016-12-26
* Work around bug in 8.4 implicitsGravatar Jason Gross2016-12-14
* Move things to ExprInversionGravatar Jason Gross2016-12-03
* Add invert_VarGravatar Jason Gross2016-12-03
* Arguments for invert_OpGravatar Jason Gross2016-12-03
* Add invert_OpGravatar Jason Gross2016-12-03
* Change some default namesGravatar Jason Gross2016-12-03
* Add SmartFlatTypeMapUnInterpGravatar Jason Gross2016-12-02
* Add invert_LetInGravatar Jason Gross2016-12-02
* Arguments for invert_PairGravatar Jason Gross2016-12-02
* Add invert_PairGravatar Jason Gross2016-12-02
* Add SmartFlatTypeMapInterpGravatar Jason Gross2016-12-02
* SmartFlatTypeMap argumentsGravatar Jason Gross2016-12-02
* Add SmartFlatTypeMapGravatar Jason Gross2016-12-02
* : assert is not valid 8.4 syntaxGravatar Jason Gross2016-11-17
* Add Un{Return,Abs}_etaGravatar Jason Gross2016-11-16
* Add : assert to a bunch of argumentsGravatar Jason Gross2016-11-16
* Split fixedpoint in interpfGravatar Jason Gross2016-11-16
* Arguments for Un{Return,Abs}Gravatar Jason Gross2016-11-16
* Add UnReturn, UnAbsGravatar Jason Gross2016-11-16
* Add flat_interp_tuple_untuple'Gravatar Jason Gross2016-11-07
* Add flat_interp_untuple'_tupleGravatar Jason Gross2016-11-07
* Add syntactic tuplesGravatar Jason Gross2016-11-06
* Add SmartVarMap_heteroGravatar Jason Gross2016-10-31
* Add some interpretations things, speed up proofs in Ed25519Gravatar Jason Gross2016-10-31
* Add [f] to things that use [exprf] or [flat_type]Gravatar Jason Gross2016-10-31
* Implicits for SmartVarMapTGravatar Jason Gross2016-10-31
* Add SmartVarMapTGravatar Jason Gross2016-10-31
* Interpret syntax with Let_InGravatar Jason Gross2016-10-31
* Generalize interp_flat_type_rel_pointwise2 a bitGravatar Jason Gross2016-10-30
* Minor reflective changesGravatar Jason Gross2016-10-30
* Add InterpWfGravatar Jason Gross2016-10-28
* Add InterpWfRelGravatar Jason Gross2016-10-28
* Add interp_type_gen_rel_pointwise2, *_gen => *Gravatar Jason Gross2016-10-28
* PHOAS notation fixupsGravatar Jason Gross2016-10-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 15:37:08 +0000