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

[stdlib] [CMorphisms] rename scope signature into signatureT #15446

Merged
merged 1 commit into from Jan 10, 2022
Merged

[stdlib] [CMorphisms] rename scope signature into signatureT #15446

merged 1 commit into from Jan 10, 2022

Conversation

olaure01
Copy link
Contributor

@olaure01 olaure01 commented Jan 7, 2022 •
edited

This avoids overridding of notations when importing CMorphisms after Setoid:

From Coq Require Import Setoid CMorphisms.
(*
Notation "_ ++> _" was already used in scope signature_scope.
[notation-overridden,parsing]
Notation "_ ==> _" was already used in scope signature_scope.
[notation-overridden,parsing]
Notation "_ --> _" was already used in scope signature_scope.
[notation-overridden,parsing]
*)

@olaure01 olaure01 added part: standard library The standard library stdlib. part: notations The notation system. kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. labels Jan 7, 2022
@olaure01 olaure01 requested a review from a team as a code owner January 7, 2022 17:00
olaure01 added a commit to olaure01/metacoq that referenced this pull request Jan 7, 2022
@olaure01
adapt to coq/coq#15446
d601c2f
@mattam82 mattam82 self-assigned this Jan 10, 2022
@mattam82
Copy link
Member

Thanks for the PR! Indeed one might need to mix the two scopes in general.

@mattam82 mattam82 added this to the 8.16+rc1 milestone Jan 10, 2022
@mattam82
Copy link
Member

@coqbot merge now

@coqbot-app coqbot-app bot merged commit b9c8d6d into coq:master Jan 10, 2022
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Jan 10, 2022

@mattam82: Please take care of the following overlays:

  • 15446-olaure01-signatureT.sh

mattam82 added a commit to MetaCoq/metacoq that referenced this pull request Jan 10, 2022
@mattam82
Merge pull request #628 from olaure01/signatureT
717d48c 
adapt to coq/coq#15446
mattam82 added a commit to MetaCoq/metacoq that referenced this pull request Feb 8, 2022
@mattam82
Revert "adapt to coq/coq#15446"
e32e1ad 
This reverts commit d601c2f.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@mattam82 mattam82 mattam82 approved these changes

Assignees

@mattam82 mattam82

Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: notations The notation system. part: standard library The standard library stdlib.
Projects
None yet
Milestone
8.16+rc1
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@olaure01 @mattam82