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: use preterm in exact / eexact #18157

Merged
merged 1 commit into from
Nov 18, 2023
Merged

Ltac2: use preterm in exact / eexact #18157

merged 1 commit into from
Nov 18, 2023

Commits on Nov 13, 2023

  1. Ltac2: use preterm in exact / eexact 

    Fix coq#12827

The implementation uses a generalization of Constr.pretype which takes
flags (an opaque type) and a typing constraint.

Changing `refine` is left to the future as the notation takes a tactic
thunk at constr type so would be backwards incompatible.
    @SkySkimmer
    SkySkimmer committed Nov 13, 2023
    Configuration menu
    Copy the full SHA
    3451f1f View commit details
    Browse the repository at this point in the history