From a3bcb51ef1be5a856078d1a3388ad38aa9b5cdc0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 20 Feb 2019 22:43:40 +0100
Subject: [PATCH] tweak proofs

---
 theories/numbers.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/numbers.v b/theories/numbers.v
index e2835d81..2455887c 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 try done.
+Next Obligation. done. Qed.
 Next Obligation. intros x y; apply Qcle_not_lt. Qed.
 
 Instance: PartialOrder (≤).
-- 
GitLab