diff --git a/_CoqProject b/_CoqProject
index a38be24..7c948da 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -5,6 +5,7 @@
 -arg -w -arg -redundant-canonical-projection
 -arg -w -arg -deprecated-hint-without-locality
 -arg -w -arg -deprecated-instance-without-locality
+-arg -w -arg -rewrite-rw
 
 theories/reals/real.v
 theories/reals/realsyntax.v
diff --git a/theories/proof/part.v b/theories/proof/part.v
index db49dcb..e8ceeb4 100644
--- a/theories/proof/part.v
+++ b/theories/proof/part.v
@@ -197,10 +197,10 @@ Notation "7 ? 8" := Pr78 (at level 0, format "7 ? 8") : prange_scope.
 
 Bind Scope part_scope with part.
 
-Arguments Pcons (spk hat)%prange_scope p%part_scope.
-Arguments Pcons6 (hat fan1)%prange_scope p%part_scope.
-Arguments Pcons7 (hat fan1 fan2)%prange_scope p%part_scope.
-Arguments Pcons8 (hat fan1 fan2 fan3)%prange_scope p%part_scope.
+Arguments Pcons (spk hat)%_prange_scope p%_part_scope.
+Arguments Pcons6 (hat fan1)%_prange_scope p%_part_scope.
+Arguments Pcons7 (hat fan1 fan2)%_prange_scope p%_part_scope.
+Arguments Pcons8 (hat fan1 fan2 fan3)%_prange_scope p%_part_scope.
 
 Definition Part (p : part) := p.
 
diff --git a/theories/proof/present.v b/theories/proof/present.v
index 3f5c193..38c2ca8 100644
--- a/theories/proof/present.v
+++ b/theories/proof/present.v
@@ -216,8 +216,8 @@ Arguments succeed_by_hubcap hc {p0 p} red_check _ _ {G x}.
 
 Export PartSyntax.
 
-Arguments succeeds_in (p0 p)%part_scope.
-Arguments successful p%part_scope.
+Arguments succeeds_in (p0 p)%_part_scope.
+Arguments successful p%_part_scope.
 
 Notation "'Check' p1 'in' p0" := (succeeds_in p0 p1)
   (at level 10, p1, p0 at level 9,
diff --git a/theories/reals/realsyntax.v b/theories/reals/realsyntax.v
index 270d1a4..63b3e1e 100644
--- a/theories/reals/realsyntax.v
+++ b/theories/reals/realsyntax.v
@@ -46,24 +46,24 @@ Local Open Scope real_scope.
 Arguments val R : rename, simpl never.
 Arguments set R : rename, simpl never.
 Arguments rel R : rename, simpl never.
-Arguments le {R} x%Rval y%Rval : rename, simpl never.
-Arguments sup {R} E%Rset : rename, simpl never.
-Arguments add {R} x%Rval y%Rval : rename, simpl never.
-Arguments opp {R} x%Rval : rename, simpl never.
-Arguments mul {R} x%Rval y%Rval : rename, simpl never.
-Arguments inv {R} x%Rval : rename, simpl never.
-Arguments eq {R} x%Rval y%Rval.
-Arguments ub {R} E%Rset x%Rval.
-Arguments down {R} E%Rset x%Rval.
-Arguments nonempty {R} E%Rset.
-Arguments has_ub {R} E%Rset.
-Arguments has_sup {R} E%Rset.
-Arguments image {R S} phi E%Rset y%Rval.
-Arguments nat R n%nat: simpl never.
-Arguments select_set {R} P%type x%Rval y%Rval _%Rval.
-Arguments select {R} P%type x%Rval y%Rval.
-Arguments extended_inv {R} x%Rval.
-Arguments extended_sup {R} E%Rset.
+Arguments le {R} x%_Rval y%_Rval : rename, simpl never.
+Arguments sup {R} E%_Rset : rename, simpl never.
+Arguments add {R} x%_Rval y%_Rval : rename, simpl never.
+Arguments opp {R} x%_Rval : rename, simpl never.
+Arguments mul {R} x%_Rval y%_Rval : rename, simpl never.
+Arguments inv {R} x%_Rval : rename, simpl never.
+Arguments eq {R} x%_Rval y%_Rval.
+Arguments ub {R} E%_Rset x%_Rval.
+Arguments down {R} E%_Rset x%_Rval.
+Arguments nonempty {R} E%_Rset.
+Arguments has_ub {R} E%_Rset.
+Arguments has_sup {R} E%_Rset.
+Arguments image {R S} phi E%_Rset y%_Rval.
+Arguments nat R n%_nat: simpl never.
+Arguments select_set {R} P%_type x%_Rval y%_Rval _%_Rval.
+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 1, left associativity, format "n %:R").
 Reserved Notation "x ^-1" (at level 1, left associativity, format "x ^-1").