| Commit message (Expand) | Author | Age |
... | |
* | Revert "update coq-scripts" | Jason Gross | 2017-04-13 |
* | add CVE-2017-3732 to crypto-defects.md | Andres Erbsen | 2017-04-12 |
* | update coq-scripts | Andres Erbsen | 2017-04-12 |
* | Add commented out proof of equivalence in MxDH | Jason Gross | 2017-04-12 |
* | Add denoter for symbolic_expr | Jason Gross | 2017-04-12 |
* | SOp needs to hold the type of the arguments, for denote | Jason Gross | 2017-04-12 |
* | Hold types in SFst and SSnd | Jason Gross | 2017-04-12 |
* | More comment on Saturated.v, explaining representation and the [compact] oper... | jadep | 2017-04-11 |
* | More WIP on CSE interp | Jason Gross | 2017-04-11 |
* | Extend cse context when inlining | Jason Gross | 2017-04-11 |
* | Add initial version of CSE interp | Jason Gross | 2017-04-11 |
* | Generalize prepend_prefix | Jason Gross | 2017-04-10 |
* | Fix missing 'by tac' in rewrite_hyp | Jason Gross | 2017-04-10 |
* | Finish CSE_Wf | Jason Gross | 2017-04-10 |
* | Finish most of wf for CSE | Jason Gross | 2017-04-10 |
* | Reorder parameters for ease of partial instantiation, add symbolic_expr_dec | Jason Gross | 2017-04-10 |
* | Add dec_of_bool_dec | Jason Gross | 2017-04-10 |
* | Add lookupb_extendb_full | Jason Gross | 2017-04-10 |
* | Fix CSE to correctly symbolize expressions | Jason Gross | 2017-04-10 |
* | Relax extendb, and prove a property about length | Jason Gross | 2017-04-10 |
* | Key on flat_type not base_type, in CSE | Jason Gross | 2017-04-10 |
* | Add flatten_binding_list_SmartVarfMap2_pair_In_split | Jason Gross | 2017-04-10 |
* | Add flatten_binding_list_SmartVarfMap2_pair_same_in_eq2 | Jason Gross | 2017-04-10 |
* | Use Named.Context in CSE, so we can reuse context lemmas | Jason Gross | 2017-04-10 |
* | Add AListContext, WeakListContext | Jason Gross | 2017-04-10 |
* | Split off Compilers.Named.Context | Jason Gross | 2017-04-10 |
* | Add rewrite_hyp ... by tac | Jason Gross | 2017-04-10 |
* | Finish the last of the admits in word-size-selection! | Jason Gross | 2017-04-09 |
* | Split off ZUtil.Stabilization, finish IsBoundedBy! | Jason Gross | 2017-04-09 |
* | Add Z.lt_le_flip_Proper_flip_impl | Jason Gross | 2017-04-09 |
* | More wip on bounds | Jason Gross | 2017-04-09 |
* | Add Z.pow_nonneg to zarith | Jason Gross | 2017-04-09 |
* | More progress on bounds | Jason Gross | 2017-04-09 |
* | Don't take abs in upper_lor_and_bounds | Jason Gross | 2017-04-09 |
* | Make replace_with_neg more powerful | Jason Gross | 2017-04-09 |
* | Handle more things in Z.peel_le | Jason Gross | 2017-04-09 |
* | Take more abs in Bounds.Interpretation | Jason Gross | 2017-04-09 |
* | Add Z.peel_le | Jason Gross | 2017-04-09 |
* | Factor out Z.{lor,land} proofs a bit more | Jason Gross | 2017-04-09 |
* | Add Z.log2_up_le_mono to zarith | Jason Gross | 2017-04-09 |
* | Add Z.max_le_compat Z.min_le_compat to zarith | Jason Gross | 2017-04-09 |
* | Finish shift cases, extract out land, lor facts | Jason Gross | 2017-04-09 |
* | Add lemmas about shift bounds to ZUtil | Jason Gross | 2017-04-09 |
* | Fix missing unfold | Jason Gross | 2017-04-09 |
* | Add sub_le_flip_le_Proper | Jason Gross | 2017-04-09 |
* | Makefile fixes | Jason Gross | 2017-04-09 |
* | Fix vo_reverse_closure | Jason Gross | 2017-04-09 |
* | Fix printreversedeps | Jason Gross | 2017-04-09 |
* | Add printreversedeps | Jason Gross | 2017-04-09 |
* | WIP on bounds lemma | Jason Gross | 2017-04-08 |