From a3a4c80fe628b8f17bd8a82b4651fa01ad5375ea Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 15 Jun 2018 21:28:59 +0200
Subject: [PATCH] Move comment about `IsCons` and `IsApp`.

---
 theories/proofmode/class_instances_bi.v | 3 ---
 theories/proofmode/classes.v            | 3 +++
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index 70692eb2e..1d6be838a 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -713,9 +713,6 @@ Proof.
   by rewrite sep_and intuitionistically_and and_sep_intuitionistically.
 Qed.
 
-(* We use [IsCons] and [IsApp] to make sure that [frame_big_sepL_cons] and
-[frame_big_sepL_app] cannot be applied repeatedly often when having
-[ [∗ list] k ↦ x ∈ ?e, Φ k x] with [?e] an evar. *)
 Global Instance into_sep_big_sepL_cons {A} (Φ : nat → A → PROP) l x l' :
   IsCons l x l' →
   IntoSep ([∗ list] k ↦ y ∈ l, Φ k y)
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 1a3f40433..b4cafc484 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -277,6 +277,9 @@ Hint Mode AddModal + - ! ! : typeclass_instances.
 Lemma add_modal_id {PROP : bi} (P Q : PROP) : AddModal P P Q.
 Proof. by rewrite /AddModal wand_elim_r. Qed.
 
+(** We use the classes [IsCons] and [IsApp] to make sure that instances such as
+[frame_big_sepL_cons] and [frame_big_sepL_app] cannot be applied repeatedly
+often when having [ [∗ list] k ↦ x ∈ ?e, Φ k x] with [?e] an evar. *)
 Class IsCons {A} (l : list A) (x : A) (k : list A) := is_cons : l = x :: k.
 Class IsApp {A} (l k1 k2 : list A) := is_app : l = k1 ++ k2.
 Global Hint Mode IsCons + ! - - : typeclass_instances.
-- 
GitLab