Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - refactor(library): decouple algebraic hierarchy from core lib #229

Closed
wants to merge 97 commits into from
Closed

[Merged by Bors] - refactor(library): decouple algebraic hierarchy from core lib #229

wants to merge 97 commits into from

Commits on May 11, 2020

  1. Remove norm_num

    @jcommelin
    jcommelin committed May 11, 2020
    Configuration menu
    Copy the full SHA
    e55c7e1 View commit details
    Browse the repository at this point in the history

  2. Remove a bunch of tests

    @jcommelin
    jcommelin committed May 11, 2020
    Configuration menu
    Copy the full SHA
    a349f31 View commit details
    Browse the repository at this point in the history

  3. And remove another test

    @jcommelin
    jcommelin committed May 11, 2020
    Configuration menu
    Copy the full SHA
    b1c6ca1 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/master' into remove-norm-num

    @jcommelin
    jcommelin committed May 11, 2020
    Configuration menu
    Copy the full SHA
    93ac6c4 View commit details
    Browse the repository at this point in the history

  5. Regenerate constants

    @jcommelin
    jcommelin committed May 11, 2020
    Configuration menu
    Copy the full SHA
    864a425 View commit details
    Browse the repository at this point in the history

  6. Make import lines start with 'import'

    @jcommelin
    jcommelin committed May 11, 2020
    Configuration menu
    Copy the full SHA
    7774d40 View commit details
    Browse the repository at this point in the history

  7. Decouple algebraic hierarchy from core lib

    @jcommelin
    jcommelin committed May 11, 2020
    Configuration menu
    Copy the full SHA
    83a50a5 View commit details
    Browse the repository at this point in the history

  8. Merge branch 'master' into strip-algebra

    @jcommelin
    jcommelin committed May 11, 2020
    Configuration menu
    Copy the full SHA
    5c41ca3 View commit details
    Browse the repository at this point in the history

  9. Remove unshackled files

    @jcommelin
    jcommelin committed May 11, 2020
    Configuration menu
    Copy the full SHA
    55ddbbc View commit details
    Browse the repository at this point in the history

Commits on May 12, 2020

  1. Remove commented code

    @jcommelin
    jcommelin committed May 12, 2020
    Configuration menu
    Copy the full SHA
    ee2c42f View commit details
    Browse the repository at this point in the history

  2. Remove a test

    @jcommelin
    jcommelin committed May 12, 2020
    Configuration menu
    Copy the full SHA
    b7f8b57 View commit details
    Browse the repository at this point in the history

Commits on May 13, 2020

  1. Revert "Remove commented code" 

    This reverts commit ee2c42f.
    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    8a9d32d View commit details
    Browse the repository at this point in the history

  2. Revert "Remove unshackled files" 

    This reverts commit 55ddbbc.
    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    97a0088 View commit details
    Browse the repository at this point in the history

  3. wip

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    23f9ca8 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'master' into strip-algebra

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    b249cba View commit details
    Browse the repository at this point in the history

  5. Hooray, we're compiling again

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    0449851 View commit details
    Browse the repository at this point in the history

  6. Remove unshackled files

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    83cf72d View commit details
    Browse the repository at this point in the history

  7. Fix constants

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    1a190f3 View commit details
    Browse the repository at this point in the history

  8. Remove unused code.

    @gebner
    gebner committed May 13, 2020
    Configuration menu
    Copy the full SHA
    245b721 View commit details
    Browse the repository at this point in the history

  9. Revert "Remove a test" 

    This reverts commit b7f8b57.
    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    9b0c7cd View commit details
    Browse the repository at this point in the history

  10. Fix the first test

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    96a135e View commit details
    Browse the repository at this point in the history

  11. Update test 1862

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    21112da View commit details
    Browse the repository at this point in the history

  12. Update test 1898

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    d0146ca View commit details
    Browse the repository at this point in the history

  13. Update test 1952

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    ec8a62e View commit details
    Browse the repository at this point in the history

  14. Update test bad_end_error_pos

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    961a2ae View commit details
    Browse the repository at this point in the history

  15. Update test field_type_mismatch

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    208ab57 View commit details
    Browse the repository at this point in the history

  16. Update test get_unused_name

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    9d152e9 View commit details
    Browse the repository at this point in the history

  17. Update test nested_match

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    ae63119 View commit details
    Browse the repository at this point in the history

  18. Update test out_param_proj

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    243e7a1 View commit details
    Browse the repository at this point in the history

  19. Update test quote_error_pos

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    fc414d8 View commit details
    Browse the repository at this point in the history

  20. Update test rquote

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    33bb06e View commit details
    Browse the repository at this point in the history

  21. Update test simp_symm

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    4984748 View commit details
    Browse the repository at this point in the history

  22. Update test task

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    b6744bc View commit details
    Browse the repository at this point in the history

  23. Fix expected output of nested_match

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    f5d6090 View commit details
    Browse the repository at this point in the history

  24. Update test type_context

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    fe4b8c4 View commit details
    Browse the repository at this point in the history

  25. Update test vm_override

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    00e7e25 View commit details
    Browse the repository at this point in the history

  26. Update run test 1675

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    1dd6bdd View commit details
    Browse the repository at this point in the history

  27. Update run test 1442

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    c7a784e View commit details
    Browse the repository at this point in the history

  28. Update run test 1685

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    8418586 View commit details
    Browse the repository at this point in the history

  29. Update run test ac_refl1

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    c1aa6c5 View commit details
    Browse the repository at this point in the history

  30. Update run test add_semi

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    0eca641 View commit details
    Browse the repository at this point in the history

  31. Update run test auto_param_in_structures

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    0416b9e View commit details
    Browse the repository at this point in the history

  32. Update run test auto_quote1

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    83808cc View commit details
    Browse the repository at this point in the history

  33. Update run test bin_tree

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    8a86880 View commit details
    Browse the repository at this point in the history

  34. Update run test conv_tact1

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    97794a1 View commit details
    Browse the repository at this point in the history

  35. Fix a bunch of cc run tests

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    f7f097a View commit details
    Browse the repository at this point in the history

  36. Fix run test mario_type_context

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    e5c5df5 View commit details
    Browse the repository at this point in the history

  37. Fix run test local_attribute

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    7b2f7e6 View commit details
    Browse the repository at this point in the history

  38. Fix run test interactive1

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    f3a0e36 View commit details
    Browse the repository at this point in the history

  39. Fix run test mrw

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    00a339e View commit details
    Browse the repository at this point in the history

  40. Fix run test funext_tactic

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    13edd11 View commit details
    Browse the repository at this point in the history

  41. Fix run test hand_then

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    d6bee26 View commit details
    Browse the repository at this point in the history

  42. Fix run test show_goal

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    74c0217 View commit details
    Browse the repository at this point in the history

  43. Fix run test sebastian_coe_simp

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    956f322 View commit details
    Browse the repository at this point in the history

  44. Fix run tests hinst_lemma(s)1

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    23564c1 View commit details
    Browse the repository at this point in the history

  45. Fix run test eq_cases_on

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    9c03765 View commit details
    Browse the repository at this point in the history

  46. Fix run test intros_defeq_canonizer_bug

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    9f41176 View commit details
    Browse the repository at this point in the history

  47. Fix run test dsimp_options

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    93a3fe9 View commit details
    Browse the repository at this point in the history

  48. Fix run test dsimp_proj

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    6a47cdf View commit details
    Browse the repository at this point in the history

  49. Fix interactive test goal_info

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    c6c54cc View commit details
    Browse the repository at this point in the history

  50. Fix test 1898

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    9a3f472 View commit details
    Browse the repository at this point in the history

  51. Fix expected output for tests/lean/quote_error_pos.lean

    @jcommelin
    jcommelin committed May 13, 2020
    Configuration menu
    Copy the full SHA
    a6f8119 View commit details
    Browse the repository at this point in the history

Commits on May 14, 2020

  1. Fix run test rw1

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    926ba81 View commit details
    Browse the repository at this point in the history

  2. Fix run test psum_wf_rec

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    bd6c3c3 View commit details
    Browse the repository at this point in the history

  3. Hopefully fix interactive test goal_info

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    3268769 View commit details
    Browse the repository at this point in the history

  4. Fix run test simp_tc_err

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    bc1c8a7 View commit details
    Browse the repository at this point in the history

  5. Fix run test simp_zeta

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    6621ed9 View commit details
    Browse the repository at this point in the history

  6. Fix expected output of test get_unused_name

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    c2edac9 View commit details
    Browse the repository at this point in the history

  7. Fix expected output of test type_context

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    4c480a9 View commit details
    Browse the repository at this point in the history

  8. Fix run test u_eq_max_u_v

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    c9c9ac1 View commit details
    Browse the repository at this point in the history

  9. Fix run test term_app2

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    9a24ea9 View commit details
    Browse the repository at this point in the history

  10. Fix run test name_resolution_with_params_bug

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    0fd581c View commit details
    Browse the repository at this point in the history

  11. Fix run test simp_lemmas_with_mvars

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    ce986cd View commit details
    Browse the repository at this point in the history

  12. Fix run test cc_ac3

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    6e3598a View commit details
    Browse the repository at this point in the history

  13. Fix run test nat_sub_ematch

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    fdf0053 View commit details
    Browse the repository at this point in the history

  14. Fix run test smt_assert_define

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    d0b6e4e View commit details
    Browse the repository at this point in the history

  15. Fix run test smt_ematch1

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    008beb7 View commit details
    Browse the repository at this point in the history

  16. Almost fix run test smt_ematch3

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    b4209e2 View commit details
    Browse the repository at this point in the history

  17. Fix run test smt_tests

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    36afaaa View commit details
    Browse the repository at this point in the history

  18. Fix run test exhaustive_vm_impl_test

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    7682053 View commit details
    Browse the repository at this point in the history

  19. Partial fix for run test ematch_attr_to_defs

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    3883029 View commit details
    Browse the repository at this point in the history

  20. The aexp test is thoroughly broken

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    0b87e21 View commit details
    Browse the repository at this point in the history

  21. Workaround nasty issues in aexp test

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    830947d View commit details
    Browse the repository at this point in the history

  22. Fix run test cc_ac5, thanks Mario

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    512e797 View commit details
    Browse the repository at this point in the history

  23. Almost fixed run test ematch2

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    ff22d1c View commit details
    Browse the repository at this point in the history

  24. Fix run test smt_ematch_alg_issue

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    7076b9e View commit details
    Browse the repository at this point in the history

  25. Fix run test simp_lemma_issue

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    4ff4ece View commit details
    Browse the repository at this point in the history

  26. Fix run test ematch2

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    5ee4e4f View commit details
    Browse the repository at this point in the history

  27. Remove example in run test using_smt2

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    1a3031c View commit details
    Browse the repository at this point in the history

  28. Remove 4 failing tests

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    9ff741d View commit details
    Browse the repository at this point in the history

  29. Fix test 123-2

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    82d875d View commit details
    Browse the repository at this point in the history

  30. Merge branch 'master' into strip-algebra

    @jcommelin
    jcommelin committed May 14, 2020
    Configuration menu
    Copy the full SHA
    6260f1b View commit details
    Browse the repository at this point in the history

Commits on May 15, 2020

  1. Remove a lot of dead code, put gcd back in core

    @jcommelin
    jcommelin committed May 15, 2020
    Configuration menu
    Copy the full SHA
    2b5d4bf View commit details
    Browse the repository at this point in the history

  2. Revert "Fix run test exhaustive_vm_impl_test" 

    This reverts commit 7682053.
    @jcommelin
    jcommelin committed May 15, 2020
    Configuration menu
    Copy the full SHA
    02b8bcd View commit details
    Browse the repository at this point in the history

  3. Remove more commented code

    @jcommelin
    jcommelin committed May 15, 2020
    Configuration menu
    Copy the full SHA
    aec23b2 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/master' into strip-algebra

    @jcommelin
    jcommelin committed May 15, 2020
    Configuration menu
    Copy the full SHA
    3a09238 View commit details
    Browse the repository at this point in the history

  5. Fix run test 236c

    @jcommelin
    jcommelin committed May 15, 2020
    Configuration menu
    Copy the full SHA
    c2787f2 View commit details
    Browse the repository at this point in the history