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

Ltac2: importing a mutable definition does not undo its mutations #18713

Merged
merged 3 commits into from Apr 2, 2024
Merged

Ltac2: importing a mutable definition does not undo its mutations #18713

merged 3 commits into from Apr 2, 2024

Commits on Mar 18, 2024

  1. Ltac2: importing a mutable definition does not undo its mutations 

    cf coq#10556

The previous behaviour can be gotten by doing eg

~~~coq
(* auxiliary definition to avoid repeating it, if it's a simple expression it can also be inlined *)
Ltac2 original_def := ...

Ltac2 mutable the_def := original_def.

Ltac2 Set the_def := original_def.
~~~

instead of `Ltac2 mutable the_def := ...`.
    @SkySkimmer
    SkySkimmer committed Mar 18, 2024
    Configuration menu
    Copy the full SHA
    2e0aced View commit details
    Browse the repository at this point in the history

  2. Add test for Ltac2 mutable definitions vs Import/Export 

    This exposes some complex behaviour around repeated imports when using
`Set as`.
    @SkySkimmer
    SkySkimmer committed Mar 18, 2024
    Configuration menu
    Copy the full SHA
    dce238d View commit details
    Browse the repository at this point in the history

  3. Document locality of Ltac2 Set

    @SkySkimmer
    SkySkimmer committed Mar 18, 2024
    Configuration menu
    Copy the full SHA
    5dea992 View commit details
    Browse the repository at this point in the history