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

Lra #54

Merged
merged 11 commits into from
Nov 22, 2022
Merged

Lra #54

merged 11 commits into from
Nov 22, 2022

Commits on Nov 22, 2022

  1. Add lra tactic 

    Works for any realFieldType
    @proux01 @pi8027
    proux01 authored and pi8027 committed Nov 22, 2022
    Configuration menu
    Copy the full SHA
    3f40a02 View commit details
    Browse the repository at this point in the history

  2. Handle hypotheses in lra

    @proux01 @pi8027
    proux01 authored and pi8027 committed Nov 22, 2022
    Configuration menu
    Copy the full SHA
    ef0674f View commit details
    Browse the repository at this point in the history

  3. Handle non Prop goals in lra

    @proux01 @pi8027
    proux01 authored and pi8027 committed Nov 22, 2022
    Configuration menu
    Copy the full SHA
    a90013e View commit details
    Browse the repository at this point in the history

  4. Handle large constants in lra

    @proux01 @pi8027
    proux01 authored and pi8027 committed Nov 22, 2022
    Configuration menu
    Copy the full SHA
    9c2c38c View commit details
    Browse the repository at this point in the history

  5. Add nra and psatz

    @proux01 @pi8027
    proux01 authored and pi8027 committed Nov 22, 2022
    Configuration menu
    Copy the full SHA
    b8b8fd8 View commit details
    Browse the repository at this point in the history

  6. Handle realDomainType in lra/nra/psatz 

    If a realFieldType is found, rationals are considered as constants,
otherwise a realDomainType is looked for and only integer constants
are considered.
    @proux01 @pi8027
    proux01 authored and pi8027 committed Nov 22, 2022
    Configuration menu
    Copy the full SHA
    4b84352 View commit details
    Browse the repository at this point in the history

  7. Handle morphisms 

    Following the method described in the paper
Kazuhiko Sakaguchi
Reflexive tactics for algebra, revisited
    @proux01 @pi8027
    proux01 authored and pi8027 committed Nov 22, 2022
    Configuration menu
    Copy the full SHA
    96ad04b View commit details
    Browse the repository at this point in the history

  8. Compatibility with Coq <= 8.15 

    This is a bit hackish and slower (goals are reified multiple times)
but enables using lra for MathComp without waiting for 8.16 to be the
minimum required version for MathComp.
    @proux01 @pi8027
    proux01 authored and pi8027 committed Nov 22, 2022
    Configuration menu
    Copy the full SHA
    35fdd3d View commit details
    Browse the repository at this point in the history

  9. Comment out examples requiring CSDP

    @proux01 @pi8027
    proux01 authored and pi8027 committed Nov 22, 2022
    Configuration menu
    Copy the full SHA
    8cf341a View commit details
    Browse the repository at this point in the history

  10. Compatibility with MathComp 1.12

    @proux01 @pi8027
    proux01 authored and pi8027 committed Nov 22, 2022
    Configuration menu
    Copy the full SHA
    1c17d58 View commit details
    Browse the repository at this point in the history

  11. Fix, remove the compat layer, and add a better support for GRing.inv

    @pi8027
    pi8027 committed Nov 22, 2022
    Configuration menu
    Copy the full SHA
    df4106b View commit details
    Browse the repository at this point in the history