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

Use a typeclass for non informative types #27

Merged
merged 4 commits into from
Mar 22, 2024
Merged

Use a typeclass for non informative types #27

merged 4 commits into from
Mar 22, 2024

Commits on Mar 21, 2024

  1. Lib/Checker: use a class for non_informative types 

    Leveraging the new call_subtac primitive to call the typeclass
resolution tactic and obtain a well-typed dictionary.
    @mtzguido
    mtzguido committed Mar 21, 2024
    Configuration menu
    Copy the full SHA
    dccdb03 View commit details
    Browse the repository at this point in the history

  2. Checker: remove more traces of primitive handling of non_informative

    @mtzguido
    mtzguido committed Mar 21, 2024
    Configuration menu
    Copy the full SHA
    86721b8 View commit details
    Browse the repository at this point in the history

  3. snap

    @mtzguido
    mtzguido committed Mar 21, 2024
    Configuration menu
    Copy the full SHA
    9ecfcf4 View commit details
    Browse the repository at this point in the history

  4. snap

    @mtzguido
    mtzguido committed Mar 21, 2024
    Configuration menu
    Copy the full SHA
    31d0150 View commit details
    Browse the repository at this point in the history