index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
Commit message (
Expand
)
Author
Age
...
*
Add app_curried_Proper_gen as an instance
Jason Gross
2018-08-06
*
Add related_iff_app_curried
Jason Gross
2018-08-06
*
Remove fastpath for Zcast in absint
Jason Gross
2018-08-06
*
Remove thunking from abstract interpretation
Jason Gross
2018-08-06
*
Generalize interp flat lemmas
Jason Gross
2018-08-06
*
Generalize wf_interp_Proper
Jason Gross
2018-08-06
*
Finish AbsInt Wf proofs
Jason Gross
2018-08-04
*
Backwards compatible fix for some issues from https://github.com/coq/coq/pull...
Jason Gross
2018-08-04
*
Add wf for DefaultValue
Jason Gross
2018-08-03
*
Add wf_splice_list, wf_splice_list_no_order
Jason Gross
2018-08-03
*
Fix typo in previous commit
Jason Gross
2018-08-03
*
Add eq_ident_Decidable
Jason Gross
2018-08-03
*
Add reflect_list_cps_id
Jason Gross
2018-08-03
*
Better rewrite_type_transport_correct
Jason Gross
2018-08-02
*
Adjust GENERATEDIdentifiersWithoutTypesProofs.v, add eta_ident_cps_correct
Jason Gross
2018-08-02
*
Add GENERATEDIdentifiersWithoutTypesProofs.v
Jason Gross
2018-08-02
*
Also generate decidable equality for pattern.ident
Jason Gross
2018-08-02
*
Make wf_safe_t a bit stronger
Jason Gross
2018-08-02
*
Make ERROR_BAD_REWRITE_RULE Opaque, not Qed'ed
Jason Gross
2018-08-02
*
Generalize option_eq to support heterogenous relations
Jason Gross
2018-08-02
*
Add nth_error_combine
Jason Gross
2018-08-01
*
More precise wf_Proper_list_impl
Jason Gross
2018-07-31
*
Comment out wf_splice_list
Jason Gross
2018-07-31
*
Add wf_Proper_list, wf_splice_list
Jason Gross
2018-07-31
*
Add type.related_hetero
Jason Gross
2018-07-30
*
Fix some issues in previous commit
Jason Gross
2018-07-30
*
Add nat_rect_Proper_nondep_gen
Jason Gross
2018-07-30
*
Allow proving force ∘ thunk = id extensionally
Jason Gross
2018-07-30
*
Add UnderLets.wf_Proper_list
Jason Gross
2018-07-30
*
Add wf_splice
Jason Gross
2018-07-30
*
Generalize type.eqv a bit
Jason Gross
2018-07-30
*
Some WIP on Rewiter correctness
Jason Gross
2018-07-30
*
Integrate Wf and Interp proofs
Jason Gross
2018-07-30
*
Add wf and interp proofs for LetBindReturn
Jason Gross
2018-07-27
*
More proofs about wf / interp
Jason Gross
2018-07-27
*
Add wf about reify/reflect list
Jason Gross
2018-07-27
*
Stronger inversion
Jason Gross
2018-07-27
*
Add invert_nil, invert_cons
Jason Gross
2018-07-27
*
Set arguments of ident.{gen_,}interp
Jason Gross
2018-07-27
*
Move rewrites to the correct tactic
Jason Gross
2018-07-26
*
Shuffle transport lemmas around, add more inversion
Jason Gross
2018-07-26
*
Add Wf proofs about MiscCompilerPasses
Jason Gross
2018-07-26
*
Move the associator pass to the rewriter
Jason Gross
2018-07-26
*
Improve wf tactics
Jason Gross
2018-07-26
*
Minor improvements to wf framework
Jason Gross
2018-07-26
*
Move some tactics to their proper place
Jason Gross
2018-07-26
*
Add Wf lemmas about SubstVar
Jason Gross
2018-07-26
*
Put == in type_scope, so that we don't need to go around opening etype_scope
Jason Gross
2018-07-26
*
Add basic wf proofs
Jason Gross
2018-07-26
*
Actually improve expr.invert_one
Jason Gross
2018-07-26
[prev]
[next]