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
*
Fix build
Jason Gross
2016-11-03
*
More relatedness
Jason Gross
2016-11-03
*
Make apply things go through interp_flat_type
Jason Gross
2016-11-03
*
Make apply things go through interp_flat_type
Jason Gross
2016-11-03
*
Versions of [Apply] that guarantee flat things
Jason Gross
2016-11-03
*
Add more relatedness things
Jason Gross
2016-11-03
*
Work around divergence of unification in Coq 8.5{,pl1}
Jason Gross
2016-11-02
*
Write code to lift option types over tuples
Jason Gross
2016-11-02
*
Fix bounds on neg in interpretations
Jason Gross
2016-11-02
*
Prove fe25519WToZ_ZToW, rename FooToBarToFoo to BarToFoo_FooToBar
Jason Gross
2016-11-01
*
Fix and prove bounds for cmovne, cmovle; note a problem with the neg bound
Jason Gross
2016-11-01
*
Work around bug #5175 in 8.6
Jason Gross
2016-11-01
*
Add version of [Apply] for [Interp] things
Jason Gross
2016-10-31
*
Add Reflection.Application
Jason Gross
2016-10-31
*
Add SmartVarMap_hetero
Jason Gross
2016-10-31
*
Add some interpretations things, speed up proofs in Ed25519
Jason Gross
2016-10-31
*
Add [f] to things that use [exprf] or [flat_type]
Jason Gross
2016-10-31
*
Implicits for SmartVarMapT
Jason Gross
2016-10-31
*
Add SmartVarMapT
Jason Gross
2016-10-31
*
Safer definitions of shl, shr
Jason Gross
2016-10-31
*
Fix a typo making word calculations wrong
Jason Gross
2016-10-31
*
Interpret syntax with Let_In
Jason Gross
2016-10-31
*
Also construct relatedness proofs in reified
Jason Gross
2016-10-30
*
Fix tactic notation scope in the 8.5 build
Jason Gross
2016-10-30
*
Remove an [About]
Jason Gross
2016-10-30
*
Renaming in Reflection/Z/Interpretations.v, admitted rel lemmas
Jason Gross
2016-10-30
*
Switch to a faster way of proving wf
Jason Gross
2016-10-30
*
Generalize interp_flat_type_rel_pointwise2 a bit
Jason Gross
2016-10-30
*
Minor changes to GF25519 reflective
Jason Gross
2016-10-30
*
Handle 4 arguments in Reify
Jason Gross
2016-10-30
*
Revert "Premature optimization of [Reify_rhs]"
Jason Gross
2016-10-30
*
Premature optimization of [Reify_rhs]
Jason Gross
2016-10-30
*
Fix slowness in [Defined] after [Reify_rhs]
Jason Gross
2016-10-30
*
Make Z Reification handle correctness proofs
Jason Gross
2016-10-30
*
Factor out prove_compile_correct
Jason Gross
2016-10-30
*
Adjust arguments to InputSyntax.Compile
Jason Gross
2016-10-30
*
Generalize Reify a bit
Jason Gross
2016-10-30
*
Generalize InputSyntax.Compile_correct
Jason Gross
2016-10-30
*
Factor Reify_rhs so that it's more reusable
Jason Gross
2016-10-30
*
Minor reflective changes
Jason Gross
2016-10-30
*
Fix an infinite loop
Jason Gross
2016-10-29
*
Handle Let_In in reification
Jason Gross
2016-10-29
*
Fix type reification
Jason Gross
2016-10-29
*
Finer grained type reification
Jason Gross
2016-10-29
*
More 8.4 fixes
Jason Gross
2016-10-29
*
Fix for 8.4
Jason Gross
2016-10-29
*
Finish proof in src/Reflection/InlineWf.v
Jason Gross
2016-10-29
*
Add more WfProofs
Jason Gross
2016-10-29
*
Add InterpWf
Jason Gross
2016-10-28
*
Add InterpWfRel
Jason Gross
2016-10-28
[next]