Make unscoped.v compatible with double-blind review #25

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

Open

yforster wants to merge 1 commit into rocq-9.0 from yforster-patch-1

Open

Make unscoped.v compatible with double-blind review

Annotations

11 warnings

Failed to remove 'http.https://github.com/.extraheader' from the git config

Notation List.map_length is deprecated since 8.20.

Notations "[ _ ; _ ]" defined at level 1 with arguments constr,

Notations "[ _ ; _ ]" defined at level 1 and "[ ]"

Notation "_ __tm" was already used in scope subst_scope.

Notation "_ ⟨ _ ⟩" was already used in scope subst_scope.

Notation "⟨ _ ⟩" was already used in scope fscope.

Notation "_ [ _ ]" was already used in scope subst_scope.