From ac3cee05d591b7739bed2267a3e7a5f261012349 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 19 Jan 2019 17:27:45 +0000
Subject: [PATCH] silence fewer warnings, add comment about overwriting
 notation

---
 _CoqProject        | 2 +-
 theories/numbers.v | 2 ++
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/_CoqProject b/_CoqProject
index 8d1bfd22..4e3d259b 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 75c16661..a94318ef 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.
-- 
GitLab