From 095086fe7ee6ecb4e2789e623ff9315a45e223f6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 2 Aug 2016 16:34:49 +0200
Subject: [PATCH] Fix framing under conjunctions.

---
 proofmode/class_instances.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index b430be504..dfa04ffe4 100644
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -219,7 +219,7 @@ Global Instance make_and_true_l P : MakeAnd True P P.
 Proof. by rewrite /MakeAnd left_id. Qed.
 Global Instance make_and_true_r P : MakeAnd P True P.
 Proof. by rewrite /MakeAnd right_id. Qed.
-Global Instance make_and_default P Q : MakeSep P Q (P ★ Q) | 100.
+Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
 Proof. done. Qed.
 Global Instance frame_and_l R P1 P2 Q Q' :
   Frame R P1 Q → MakeAnd Q P2 Q' → Frame R (P1 ∧ P2) Q' | 9.
-- 
GitLab