From edbe48a74fe33be607d74c5c8c07a04cf73555eb Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 29 Jan 2019 11:05:42 +0100
Subject: [PATCH] fix or silence Coq 8.10 warnings

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

diff --git a/_CoqProject b/_CoqProject
index 735493d4..c79d1211 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,4 +1,6 @@
 -Q theories stdpp
+# "Declare Scope" does not exist yet in 8.9
+-arg -w -arg -undeclared-scope
 theories/base.v
 theories/tactics.v
 theories/option.v
diff --git a/theories/numbers.v b/theories/numbers.v
index 1ef1721d..e2835d81 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -399,7 +399,7 @@ Next Obligation. intros x y; apply Qclt_not_le. Qed.
 Next Obligation. done. Qed.
 Program Instance Qc_lt_dec: RelDecision Qclt := λ x y,
   if Qclt_le_dec x y then left _ else right _.
-Solve Obligations with done.
+Solve Obligations with try done.
 Next Obligation. intros x y; apply Qcle_not_lt. Qed.
 
 Instance: PartialOrder (≤).
-- 
GitLab