From 6e19b458127d2e8b7e54ea81f65116a92c2a4b05 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 5 Oct 2020 19:46:41 +0200
Subject: [PATCH] better way to trigger TC search
---
theories/algebra/dfrac.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/algebra/dfrac.v b/theories/algebra/dfrac.v
index 4b2a013f6..9c7e4e32f 100644
--- a/theories/algebra/dfrac.v
+++ b/theories/algebra/dfrac.v
@@ -127,7 +127,7 @@ Section dfrac.
intros [q| |q];
rewrite /op /cmra_op -cmra_discrete_valid_iff /valid /cmra_valid /=.
- apply (Qp_not_plus_ge 1 q).
- - intros []%irreflexivity. apply _.
+ - intros []%(irreflexivity _).
- move=> /Qclt_le_weak. apply (Qp_not_plus_ge 1 q).
Qed.
--
GitLab