From 69971a15eedb4a21ff03cbd926e91110ca3af0a9 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Thu, 8 Aug 2019 00:18:47 +0200
Subject: [PATCH] Rename prop_ext to prop_ext_2

---
 theories/base_logic/bi.v    |  2 +-
 theories/base_logic/upred.v |  2 +-
 theories/bi/monpred.v       |  2 +-
 theories/bi/plainly.v       | 12 ++++++------
 4 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 1d3758f02..11a1a6a40 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -121,7 +121,7 @@ Proof.
     etrans; first exact: sep_comm'.
     apply sep_mono; last done.
     exact: pure_intro.
-  - exact: prop_ext.
+  - exact: prop_ext_2.
   - exact: later_plainly_1.
   - exact: later_plainly_2.
 Qed.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index e1b07ab63..b861d2284 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -617,7 +617,7 @@ Proof. by unseal. Qed.
 Lemma plainly_exist_1 {A} (Ψ : A → uPred M) : (■ ∃ a, Ψ a) ⊢ (∃ a, ■ Ψ a).
 Proof. by unseal. Qed.
 
-Lemma prop_ext P Q : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q.
+Lemma prop_ext_2 P Q : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q.
 Proof.
   unseal; split=> n x ? /= HPQ. split=> n' x' ??.
     move: HPQ=> [] /(_ n' x'); rewrite !left_id=> ?.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 9e9fe6a05..3ae1afcc4 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -923,7 +923,7 @@ Proof.
   - intros P. split=> i /=. apply bi.forall_intro=>_. by apply plainly_emp_intro.
   - intros P Q. split=> i. apply bi.sep_elim_l, _.
   - intros P Q. split=> i /=. rewrite (monPred_equivI P Q). f_equiv=> j.
-    by rewrite -prop_ext !(bi.forall_elim j) !bi.pure_True // !bi.True_impl.
+    by rewrite -prop_ext_2 !(bi.forall_elim j) !bi.pure_True // !bi.True_impl.
   - intros P. split=> i /=.
     rewrite bi.later_forall. f_equiv=> j. by rewrite -later_plainly_1.
   - intros P. split=> i /=.
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index b28934bcb..e8d391113 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -29,7 +29,7 @@ Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := {
   bi_plainly_mixin_plainly_emp_intro (P : PROP) : P ⊢ ■ emp;
   bi_plainly_mixin_plainly_absorb (P Q : PROP) : ■ P ∗ Q ⊢ ■ P;
 
-  bi_plainly_mixin_prop_ext (P Q : PROP) : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q;
+  bi_plainly_mixin_prop_ext_2 (P Q : PROP) : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q;
 
   bi_plainly_mixin_later_plainly_1 (P : PROP) : ▷ ■ P ⊢ ■ ▷ P;
   bi_plainly_mixin_later_plainly_2 (P : PROP) : ■ ▷ P ⊢ ▷ ■ P;
@@ -74,8 +74,8 @@ Section plainly_laws.
   Lemma plainly_emp_intro P : P ⊢ ■ emp.
   Proof. eapply bi_plainly_mixin_plainly_emp_intro, bi_plainly_mixin. Qed.
 
-  Lemma prop_ext P Q : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q.
-  Proof. eapply bi_plainly_mixin_prop_ext, bi_plainly_mixin. Qed.
+  Lemma prop_ext_2 P Q : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q.
+  Proof. eapply bi_plainly_mixin_prop_ext_2, bi_plainly_mixin. Qed.
 
   Lemma later_plainly_1 P : ▷ ■ P ⊢ ■ (▷ P).
   Proof. eapply bi_plainly_mixin_later_plainly_1, bi_plainly_mixin. Qed.
@@ -470,7 +470,7 @@ Qed.
 Lemma plainly_alt P : ■ P ⊣⊢ <affine> P ≡ emp.
 Proof.
   rewrite -plainly_affinely_elim. apply (anti_symm (⊢)).
-  - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l.
+  - rewrite -prop_ext_2. apply plainly_mono, and_intro; apply wand_intro_l.
     + by rewrite affinely_elim_emp left_id.
     + by rewrite left_id.
   - rewrite internal_eq_sym (internal_eq_rewrite _ _ plainly).
@@ -480,7 +480,7 @@ Qed.
 Lemma plainly_alt_absorbing P `{!Absorbing P} : ■ P ⊣⊢ P ≡ True.
 Proof.
   apply (anti_symm (⊢)).
-  - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
+  - rewrite -prop_ext_2. apply plainly_mono, and_intro; apply wand_intro_l; auto.
   - rewrite internal_eq_sym (internal_eq_rewrite _ _ plainly).
     by rewrite plainly_pure True_impl.
 Qed.
@@ -488,7 +488,7 @@ Qed.
 Lemma plainly_True_alt P : ■ (True -∗ P) ⊣⊢ P ≡ True.
 Proof.
   apply (anti_symm (⊢)).
-  - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
+  - rewrite -prop_ext_2. apply plainly_mono, and_intro; apply wand_intro_l; auto.
     by rewrite wand_elim_r.
   - rewrite internal_eq_sym (internal_eq_rewrite _ _
       (λ Q, ■ (True -∗ Q))%I ltac:(shelve)); last solve_proper.
-- 
GitLab