From 94a98b3fbf35fe6c821019e99afbbff9a4bee544 Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Fri, 2 Oct 2020 11:20:40 +0200
Subject: [PATCH] Change eapply to apply

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

diff --git a/theories/numbers.v b/theories/numbers.v
index ded9ee43..9c1c0ab5 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -860,7 +860,7 @@ Proof.
 Qed.
 
 Lemma Qp_plus_id_free q p : q + p = q → False.
-Proof. intro Heq. eapply (Qp_not_plus_ge q p). rewrite Heq. done. Qed.
+Proof. intro Heq. apply (Qp_not_plus_ge q p). by rewrite Heq.  Qed.
 
 Lemma Qp_plus_weak_r (q p o : Qp) : q + p ≤ o → q ≤ o.
 Proof. intros Le. eapply Qcle_trans; [ apply Qp_le_plus_l | apply Le ]. Qed.
-- 
GitLab