Adapt to math-comp/math-comp#1354

coq-community · Feb 28, 2025 · 7cea617 · 7cea617
1 parent add58b4
commit 7cea617
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 3 deletions.
diff --git a/theories/reals/realprop.v b/theories/reals/realprop.v
@@ -906,4 +906,3 @@ Existing Instance max_Proper.
 Existing Instance range1_Proper.
 Existing Instance floor_Proper.
 Existing Instance imageR_Proper.
-
diff --git a/theories/reals/realsyntax.v b/theories/reals/realsyntax.v
@@ -65,8 +65,8 @@ Arguments select {R} P%type x%Rval y%Rval.
 Arguments extended_inv {R} x%Rval.
 Arguments extended_sup {R} E%Rset.
 
-Reserved Notation "n %:R" (at level 2, left associativity, format "n %:R").
-Reserved Notation "x ^-1" (at level 3, left associativity, format "x ^-1").
+Reserved Notation "n %:R" (at level 1, left associativity, format "n %:R").
+Reserved Notation "x ^-1" (at level 1, left associativity, format "x ^-1").
 
 Reserved Notation "x == y" (at level 70, no associativity).
 Reserved Notation "x != y" (at level 70, no associativity).
Original file line number	Diff line number	Diff line change
Expand Up		@@ -906,4 +906,3 @@ Existing Instance max_Proper.
		Existing Instance range1_Proper.
		Existing Instance floor_Proper.
		Existing Instance imageR_Proper.