index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Reflection
Commit message (
Expand
)
Author
Age
*
Minor additions
Jason Gross
2017-01-23
*
Fix a typo
Jason Gross
2017-01-23
*
Add invert_expr_subst
Jason Gross
2017-01-23
*
Allow inversion on wff if either side is not a var
Jason Gross
2017-01-23
*
Remove the Const constructor of exprf
Jason Gross
2017-01-19
*
Make f_equal2 transparent in equality proof
Jason Gross
2017-01-19
*
Split out Reflection.Equality, change Tflat implicit argument
Jason Gross
2017-01-19
*
More fine-grained util tactic files
Jason Gross
2017-01-17
*
Add ApplicationRelations
Jason Gross
2017-01-10
*
Add Syntax.tuple_map
Jason Gross
2017-01-09
*
Fixes for Coq 8.4
Jason Gross
2017-01-03
*
Add src/Reflection/MapCastWithCastOp.v
Jason Gross
2017-01-01
*
Remove [Print]
Jason Gross
2017-01-01
*
Redo MultiSizeTest with generic framework
Jason Gross
2017-01-01
*
Transparent versions of {flat_,}type_eq_dec
Jason Gross
2017-01-01
*
Add generic code for MultiSizeTest
Jason Gross
2017-01-01
*
Add smart_interp_map_gen
Jason Gross
2017-01-01
*
Add SmartFlatTypeMap2
Jason Gross
2016-12-26
*
Add flatten_flat_type
Jason Gross
2016-12-26
*
Fix Coq 8.6 warnings
Jason Gross
2016-12-26
*
MultiSizeTest: a basic example of the scheme I have in mind for bounds infere...
Adam Chlipala
2016-12-25
*
Fix 8.4 build issues
Jason Gross
2016-12-15
*
Fix 8.4 issues
Jason Gross
2016-12-15
*
Work around bug in 8.4 implicits
Jason Gross
2016-12-14
*
Don't use UIP in inversion_wff
Jason Gross
2016-12-03
*
Add inversion_wff
Jason Gross
2016-12-03
*
Add WfInversion
Jason Gross
2016-12-03
*
More powerful inversion_option
Jason Gross
2016-12-03
*
Move things to ExprInversion
Jason Gross
2016-12-03
*
Add invert_Var
Jason Gross
2016-12-03
*
Arguments for invert_Op
Jason Gross
2016-12-03
*
Fewer autogenerated names
Jason Gross
2016-12-03
*
Add invert_Op
Jason Gross
2016-12-03
*
Change some default names
Jason Gross
2016-12-03
*
Initial (not fully working) version of MapWithInterpInfo
Jason Gross
2016-12-02
*
Add SmartFlatTypeMapUnInterp
Jason Gross
2016-12-02
*
Add invert_LetIn
Jason Gross
2016-12-02
*
Arguments for invert_Pair
Jason Gross
2016-12-02
*
Add invert_Pair
Jason Gross
2016-12-02
*
Add SmartFlatTypeMapInterp
Jason Gross
2016-12-02
*
SmartFlatTypeMap arguments
Jason Gross
2016-12-02
*
Add SmartFlatTypeMap
Jason Gross
2016-12-02
*
Various application lemmas
Jason Gross
2016-11-23
*
Add lemmas about application
Jason Gross
2016-11-22
*
Add interp_all_binders_for'
Jason Gross
2016-11-22
*
Remove an admit
Jason Gross
2016-11-17
*
Add interpf_LetIn
Jason Gross
2016-11-17
*
: assert is not valid 8.4 syntax
Jason Gross
2016-11-17
*
Add Un{Return,Abs}_eta
Jason Gross
2016-11-16
*
Add : assert to a bunch of arguments
Jason Gross
2016-11-16
[next]