| Commit message (Expand) | Author | Age |
|---|
| * | Add some move/transport eq lemmas |  Jason Gross | 2019-04-22 |
| * | Add push_rew_fun_dep | Jason Gross | 2019-04-22 |
| * | Add Primitive.reflect_eq_prod | Jason Gross | 2019-04-18 |
| * | Fix around coq/coq#262 | Jason Gross | 2019-04-12 |
| * | Replace the python script with Ltac code | Jason Gross | 2019-04-12 |
| * | sed s'/RewriterProofs/RewriterAll/g' | Jason Gross | 2019-04-11 |
| * | rm src/*.out, now that we no longer generate these | Jason Gross | 2019-04-11 |
| * | Make a single tactic to build the rewriter | Jason Gross | 2019-04-11 |
| * | Automate more of the rewriter, and factor out rule-specific things | Jason Gross | 2019-04-11 |
| * | Add base.reflect_{base,type}_beq and type.reflect_type_beq | Jason Gross | 2019-04-10 |
| * | Fix for Coq 8.8 | Jason Gross | 2019-04-09 |
| * | Automate more of the rewriter reification, proof | Jason Gross | 2019-04-09 |
| * | Fix for 8.8 | Jason Gross | 2019-04-05 |
| * | Generalize correctly in strip_literal_casts_rewrite_rulesT | Jason Gross | 2019-04-05 |
| * | Add some bool eqb lemmas | Jason Gross | 2019-04-05 |
| * | Don't eagerly unfold boolean functions, hopefully, in tc reflect search | Jason Gross | 2019-04-05 |
| * | Hint reflect on negb | Jason Gross | 2019-04-05 |
| * | Add interp_related lemmas | Jason Gross | 2019-04-05 |
| * | Add some more underlets lemmas | Jason Gross | 2019-04-04 |
| * | Add UnderLets flat_map interp proofs,other changes | Jason Gross | 2019-04-04 |
| * | partition -> Partition.partition to prevent confusion with List.partition |  jadep | 2019-04-03 |
| * | fix typo | jadep | 2019-04-03 |
| * | remove unnecessary imports from Primitives.v | jadep | 2019-04-03 |
| * | fix up imports in SmallExamples.v |  jadep | 2019-04-03 |
| * | update import statements | jadep | 2019-04-03 |
| * | rename some things | jadep | 2019-04-03 |
| * | fix imports and qualifiers so everything builds | jadep | 2019-04-03 |
| * | remove extraneous module identifiers | jadep | 2019-04-03 |
| * | update _CoqProject, fix indentations, and prune dependencies of new Arithmeti... | jadep | 2019-04-03 |
| * | split up Arithmetic (imports etc. not yet fixed, does not build) | jadep | 2019-04-03 |
| * | Add Z.combine_at_bitwidth | Jason Gross | 2019-04-02 |
| * | Factor out rewriter rules | Jason Gross | 2019-03-31 |
| * | Fix a non-terminated comment | Jason Gross | 2019-03-31 |
| * | Add some comments based on CR requests | Jason Gross | 2019-03-31 |
| * | Fix issue with refolding in eapply in < 8.9 | Jason Gross | 2019-03-31 |
| * | Finish reifying list lemmas | Jason Gross | 2019-03-31 |
| * | Add constr_fail and constr_fail_with | Jason Gross | 2019-03-31 |
| * | improve zero_bounds tactic | jadep | 2019-03-26 |
| * | add some hints to the global databases | jadep | 2019-03-26 |
| * | remove Derive to fix 8.7 | jadep | 2019-03-25 |
| * | fix montgomery | jadep | 2019-03-25 |
| * | remove 2: syntax so I don't break 8.7 | jadep | 2019-03-25 |
| * | fix up a messy proof | jadep | 2019-03-25 |
| * | Move some lemmas to appropriate places | jadep | 2019-03-25 |
| * | finish proofs | jadep | 2019-03-25 |
| * | Get new Barrett proofs to generate Fancy code as before | jadep | 2019-03-25 |
| * | WIP | jadep | 2019-03-25 |
| * | Add UnderLets.wf_flat_map | Jason Gross | 2019-03-12 |
| * | Add UnderLets.wf_of_expr | Jason Gross | 2019-03-09 |
| * | Add some UnderLets wf proofs | Jason Gross | 2019-03-08 |
Jason Gross
jadep
jadep