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

Adding support for recursive blocs and associativity in ARGUMENT EXTEND #12743

Closed
wants to merge 12 commits into from
Closed

Adding support for recursive blocs and associativity in ARGUMENT EXTEND #12743

wants to merge 12 commits into from

Commits on Dec 20, 2021

  1. Fixes coq#15334: anomaly on parsing error due to empty entry (8.14 re… 

    …gression).

case of failure due to an empty entry was not treated as in:

Declare Custom Entry ent.
Notation "ent:( x )" := x (x custom ent).
Notation "a ; b" := (pair a b) (in custom ent at level 50).
Check ent:(_ ; _).
    @herbelin
    herbelin committed Dec 20, 2021
    Configuration menu
    Copy the full SHA
    5723bb6 View commit details
    Browse the repository at this point in the history

  2. Changelog for coq#15338

    @herbelin
    herbelin committed Dec 20, 2021
    Configuration menu
    Copy the full SHA
    7e75b82 View commit details
    Browse the repository at this point in the history

  3. Fixes a regression in unification bug coq#3209. 

    "Fail" was not checking that the error was a Not_found in the test file.
    @herbelin
    herbelin committed Dec 20, 2021
    Configuration menu
    Copy the full SHA
    5c78242 View commit details
    Browse the repository at this point in the history

  4. Print all goals in debugger (quick fix)

    @jfehrle @herbelin
    jfehrle authored and herbelin committed Dec 20, 2021
    Configuration menu
    Copy the full SHA
    a4bfb58 View commit details
    Browse the repository at this point in the history

  5. Deprecate "dfs eauto" tactic

    @jfehrle @herbelin
    jfehrle authored and herbelin committed Dec 20, 2021
    Configuration menu
    Copy the full SHA
    edc3e80 View commit details
    Browse the repository at this point in the history

  6. Contributing guide: fix grammar mistake (less -> fewer).

    @Zimmi48 @herbelin
    Zimmi48 authored and herbelin committed Dec 20, 2021
    Configuration menu
    Copy the full SHA
    2df81ec View commit details
    Browse the repository at this point in the history

  7. Ensure at grammar level that module application is always to a qualid. 

    We keep module_expr_atom to be able to use parentheses as in
~~~coq
Module M := F (X).
~~~

However `Module M := (X Y)` seems not so nice and is dropped.
    @SkySkimmer @herbelin
    SkySkimmer authored and herbelin committed Dec 20, 2021
    Configuration menu
    Copy the full SHA
    6ea0e20 View commit details
    Browse the repository at this point in the history

  8. Adding support for associativity in ARGUMENT EXTEND.

    @herbelin
    herbelin committed Dec 20, 2021
    Configuration menu
    Copy the full SHA
    bc9323a View commit details
    Browse the repository at this point in the history

  9. Making explicit that some GRAMMAR EXTEND entries are intended to be R… 

    …IGHTA.
    @herbelin
    herbelin committed Dec 20, 2021
    Configuration menu
    Copy the full SHA
    9b9cb80 View commit details
    Browse the repository at this point in the history

  10. Making explicit the associativity of some recursive ARGUMENT EXTEND.

    @herbelin
    herbelin committed Dec 20, 2021
    Configuration menu
    Copy the full SHA
    b959487 View commit details
    Browse the repository at this point in the history

  11. Adding support for recursive blocs of ARGUMENT EXTEND. 

    TO DO:
- adapt to VERNAC ARGUMENT EXTEND
- organize the code around nicer invariants
    @herbelin
    herbelin committed Dec 20, 2021
    Configuration menu
    Copy the full SHA
    a7e57f8 View commit details
    Browse the repository at this point in the history

  12. Getting rid of ambiguity in rewstrategy grammar, using a ARGUMENT EXT… 

    …END bloc.
    @herbelin
    herbelin committed Dec 20, 2021
    Configuration menu
    Copy the full SHA
    c1bcef1 View commit details
    Browse the repository at this point in the history