From 7e802184a5b2f741441f5d4a44744815dedae553 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 31 Aug 2020 18:10:28 +0200
Subject: [PATCH] Fix compilation with Coq master due to undeclared names.

---
 theories/numbers.v | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/theories/numbers.v b/theories/numbers.v
index 5df2de4f..648b01ab 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -861,9 +861,9 @@ Proof. rewrite Qcplus_comm. apply Qp_plus_weak_2_r. Qed.
 
 Lemma Qp_max_spec (q p : Qp) : (q < p ∧ q `max` p = p) ∨ (p ≤ q ∧ q `max` p = q).
 Proof.
-  unfold Qp_max. destruct (decide (q ≤ p)).
-  - destruct (Qcle_lt_or_eq _ _ q0) as [? | ->%Qp_eq]; [left|right]; done.
-  - right. split; [|done]. by apply Qclt_le_weak, Qcnot_le_lt.
+  unfold Qp_max.
+  destruct (decide (q ≤ p)) as [[?| ->%Qp_eq]%Qcle_lt_or_eq|?]; [by auto..|].
+  right. split; [|done]. by apply Qclt_le_weak, Qcnot_le_lt.
 Qed.
 
 Lemma Qp_max_spec_le (q p : Qp) : (q ≤ p ∧ q `max` p = p) ∨ (p ≤ q ∧ q `max` p = q).
@@ -907,9 +907,9 @@ Proof. rewrite (comm _ q). apply Qp_max_lub_l. Qed.
 
 Lemma Qp_min_spec (q p : Qp) : (q < p ∧ q `min` p = q) ∨ (p ≤ q ∧ q `min` p = p).
 Proof.
-  unfold Qp_min. destruct (decide (q ≤ p)).
-  - destruct (Qcle_lt_or_eq _ _ q0) as [?| ->%Qp_eq]; [left|right]; done.
-  - right. split; [|done]. by apply Qclt_le_weak, Qcnot_le_lt.
+  unfold Qp_min.
+  destruct (decide (q ≤ p)) as [[?| ->%Qp_eq]%Qcle_lt_or_eq|?]; [by auto..|].
+  right. split; [|done]. by apply Qclt_le_weak, Qcnot_le_lt.
 Qed.
 
 Lemma Qp_min_spec_le (q p : Qp) : (q ≤ p ∧ q `min` p = q) ∨ (p ≤ q ∧ q `min` p = p).
-- 
GitLab