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.

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

Clarifying the logic of levels in custom and constr entry rules (reopening of #13025) #17117

Merged
merged 8 commits into from Jun 1, 2023

Commits on May 30, 2023

  1. Replacing some uses of "subentries" by "non-terminal" (more standard

    terminology already in used).
    herbelin authored and proux01 committed May 30, 2023
    Configuration menu
    Copy the full SHA
    547750e View commit details
    Browse the repository at this point in the history
  2. We introduce a type notation_entry_relative_level to preserve more

    informations about the subentries: we remember whether we are at any
    level, at the next level or at the self level.
    
    Incidentally, we also take into account option Printing Parentheses in
    custom entries.
    
    This is a more principled fix to coq#12775/coq#13018 than coq#13073 (printing
    bugs in custom entry rules with no explicit level).
    
    Compared to "subentries", the name "entry_relative" insists on the
    syntactic structure of the type rather than on its semantic origin,
    since, after all, subentries are promoted as entries in the recursive
    printing loop.
    herbelin authored and proux01 committed May 30, 2023
    Configuration menu
    Copy the full SHA
    820d072 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    9a79ed8 View commit details
    Browse the repository at this point in the history

Commits on May 31, 2023

  1. Configuration menu
    Copy the full SHA
    79fb3b2 View commit details
    Browse the repository at this point in the history
  2. Adjust notation tests.

    herbelin authored and proux01 committed May 31, 2023
    Configuration menu
    Copy the full SHA
    981aefa View commit details
    Browse the repository at this point in the history
  3. To make the treatment more uniform, we use levels also in constr.

    We hard-wire a coercion in constr from level 0 to the top level.
    herbelin authored and proux01 committed May 31, 2023
    Configuration menu
    Copy the full SHA
    0e7fce1 View commit details
    Browse the repository at this point in the history
  4. Add overlay for coq-elpi and serapi

    herbelin authored and proux01 committed May 31, 2023
    Configuration menu
    Copy the full SHA
    b79816f View commit details
    Browse the repository at this point in the history
  5. Adding change log for coq#17117

    herbelin authored and proux01 committed May 31, 2023
    Configuration menu
    Copy the full SHA
    43bface View commit details
    Browse the repository at this point in the history