aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/Syntax.v
Commit message (Expand)AuthorAge
* 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
* Make it easier to export only phoas notationsGravatar Jason Gross2016-10-27
* Move interp_flat_type_gen_rel_pointwise2 to SyntaxGravatar Jason Gross2016-10-27
* Add arguments to mapf_interp_flat_type_genGravatar Jason Gross2016-10-27
* Better arguments for SmartVarMapGravatar Jason Gross2016-09-18
* Arguments for SmartVarMapGravatar Jason Gross2016-09-18
* Generalize SmartVarVarGravatar Jason Gross2016-09-18
* Add reserved notation for Let, change #Gravatar Jason Gross2016-09-17
* Split off lemmas about [InlineConst]Gravatar Jason Gross2016-09-16
* Add arguments for smartvalGravatar Jason Gross2016-09-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 06:28:11 +0000