From 4179bb8acbc1101561ed4677651d86b6a6d92f2e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 9 Aug 2022 16:01:43 +0200
Subject: [PATCH] `FromAnd` is never used for `iCombine`, so remove that mode.

---
 iris/proofmode/classes.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index b13aa6abd..9596b66ca 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -180,7 +180,6 @@ Class FromAnd {PROP : bi} (P Q1 Q2 : PROP) := from_and : Q1 ∧ Q2 ⊢ P.
 Global Arguments FromAnd {_} _%I _%I _%I : simpl never.
 Global Arguments from_and {_} _%I _%I _%I {_}.
 Global Hint Mode FromAnd + ! - - : typeclass_instances.
-Global Hint Mode FromAnd + - ! ! : typeclass_instances. (* For iCombine *)
 
 (** The [IntoAnd p P Q1 Q2] class is used to handle some [[H1 H2]] intro
 patterns:
-- 
GitLab