diff --git a/_CoqProject b/_CoqProject
index 8d1bfd225caecf731bf5827eb763525c0c32dd6a..4e3d259b9d51a53d8d686e7d4663e45cea2ec0b1 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,5 +1,5 @@
 -Q theories stdpp
--arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
+-arg -w -arg -notation-overridden
 theories/base.v
 theories/tactics.v
 theories/option.v
diff --git a/theories/numbers.v b/theories/numbers.v
index 75c16661bcaa1cfe8fccd4c649ee286392d4dcd0..a94318ef1f6245f4848f398737b45c985f02225d 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -380,6 +380,8 @@ Notation "1" := (Q2Qc 1) : Qc_scope.
 Notation "2" := (1+1) : Qc_scope.
 Notation "- 1" := (Qcopp 1) : Qc_scope.
 Notation "- 2" := (Qcopp 2) : Qc_scope.
+(* The following two already exist in Coq's stdlib, but we overwrite them with a
+different definition. *)
 Notation "x - y" := (x + -y) : Qc_scope.
 Notation "x / y" := (x * /y) : Qc_scope.
 Infix "≤" := Qcle : Qc_scope.