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

Control the transparency of compatibility constants via their projections. #18373

Closed
wants to merge 10 commits into from
Closed

Control the transparency of compatibility constants via their projections. #18373

wants to merge 10 commits into from

Commits on Dec 14, 2023

  1. Improve primitive projection test-suite coverage.

    @rlepigre
    Jan-Oliver Kaiser authored and rlepigre committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    222fdb0 View commit details
    Browse the repository at this point in the history

  2. Add projection field to [TransparentState.t].

    @rlepigre
    rlepigre committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    f85e2dd View commit details
    Browse the repository at this point in the history

  3. Extend [kernel/redFlags.ml] with projection.

    @rlepigre
    rlepigre committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    f27d694 View commit details
    Browse the repository at this point in the history

  4. Add [RedFlags.red_sub_list] and [RedFlags.red_add_list].

    @rlepigre
    rlepigre committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    993758d View commit details
    Browse the repository at this point in the history

  5. Update [checker/values.ml].

    @SkySkimmer @rlepigre
    SkySkimmer authored and rlepigre committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    89f9b7e View commit details
    Browse the repository at this point in the history

  6. Add debug printer for projections.

    @rlepigre
    rlepigre committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    b4abd92 View commit details
    Browse the repository at this point in the history

  7. Use projection (debug) printers in [dev/to_printers.ml].

    @rlepigre
    rlepigre committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    29792b0 View commit details
    Browse the repository at this point in the history

  8. Introduce module [Names.Evaluable]. 

    This is a replacement for [Tacred.evaluable_global_reference].

Co-Authored-By: Jan-Oliver Kaiser <janno@bedrocksystems.com>
    @rlepigre
    rlepigre and Jan-Oliver Kaiser committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    b3fc042 View commit details
    Browse the repository at this point in the history

  9. Adapt vernac-level projections opacity setting. 

    We provide an override syntax, only meant for debugging, that
lets one set the opacity of the compatibility constant instead
of the projection (i.e., the old behaviour).
    @rlepigre
    rlepigre committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    315fec3 View commit details
    Browse the repository at this point in the history

  10. Addapt unification algorithms and tactics.

    @rlepigre
    rlepigre committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    87483bf View commit details
    Browse the repository at this point in the history