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

Controlling typing flags with commands (no attribute) #10291

Merged
merged 9 commits into from Aug 20, 2019
Merged

Controlling typing flags with commands (no attribute) #10291

merged 9 commits into from Aug 20, 2019

Commits on Aug 16, 2019

  1. Split the [check_guarded] typing_flag into [check_guarded] (for (co)f… 

    …ixpoints) and [check_positive] (for (co)inductive types).
    @SimonBoulier
    SimonBoulier committed Aug 16, 2019
    Configuration menu
    Copy the full SHA
    bc4560f View commit details
    Browse the repository at this point in the history

  2. Add [Print Typing Flags] command.

    @SimonBoulier
    SimonBoulier committed Aug 16, 2019
    Configuration menu
    Copy the full SHA
    33f7877 View commit details
    Browse the repository at this point in the history

  3. Set/Unset commands for typing flags

    @SimonBoulier
    SimonBoulier committed Aug 16, 2019
    Configuration menu
    Copy the full SHA
    abab878 View commit details
    Browse the repository at this point in the history

  4. Improve [Print Assumptions] for type-in-type and assumed positive.

    @SimonBoulier
    SimonBoulier committed Aug 16, 2019
    Configuration menu
    Copy the full SHA
    889603e View commit details
    Browse the repository at this point in the history

  5. Add a file for typing_flags in the test-suite.

    @SimonBoulier
    SimonBoulier committed Aug 16, 2019
    Configuration menu
    Copy the full SHA
    6414a2a View commit details
    Browse the repository at this point in the history

  6. Add documentation for typing flags.

    @SimonBoulier
    SimonBoulier committed Aug 16, 2019
    Configuration menu
    Copy the full SHA
    de02e40 View commit details
    Browse the repository at this point in the history

  7. Universe Checking instead of Universes Checking

    @SimonBoulier
    SimonBoulier committed Aug 16, 2019
    Configuration menu
    Copy the full SHA
    2470194 View commit details
    Browse the repository at this point in the history

  8. Fix Print Assumptions: Inductive types can have unsafe fixpoints or 

     type-in-type universes
    @SimonBoulier
    SimonBoulier committed Aug 16, 2019
    Configuration menu
    Copy the full SHA
    3ae2b23 View commit details
    Browse the repository at this point in the history

  9. Fix typing_flags in the checker 

    Now all relevant typing_flags are taken in account by the checker.
The different forms of assumptions are now printed by the checker.
    @SimonBoulier
    SimonBoulier committed Aug 16, 2019
    Configuration menu
    Copy the full SHA
    d6d8229 View commit details
    Browse the repository at this point in the history