From 669dafd2b3420753b93e49d6d3ffaac746e5f002 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 25 Jan 2017 09:57:22 +0100
Subject: [PATCH] rename fixpoint2 -> fixpointAB

---
 theories/algebra/ofe.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 5285f7ef2..2708bd6b1 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -262,7 +262,7 @@ Section fixpoint.
 End fixpoint.
 
 (** Mutual fixpoints *)
-Section fixpoint2.
+Section fixpointAB.
   Local Unset Default Proof Using.
 
   Context `{Cofe A, Cofe B, !Inhabited A, !Inhabited B}.
@@ -306,9 +306,9 @@ Section fixpoint2.
   Qed.
   Lemma fixpoint_B_unique p q : fA p q ≡ p → fB p q ≡ q → q ≡ fixpoint_B.
   Proof. intros. apply fixpoint_unique. by rewrite -fixpoint_A_unique. Qed.
-End fixpoint2.
+End fixpointAB.
 
-Section fixpoint2_ne.
+Section fixpointAB_ne.
   Context `{Cofe A, Cofe B, !Inhabited A, !Inhabited B}.
   Context (fA fA' : A → B → A).
   Context (fB fB' : A → B → B).
@@ -340,7 +340,7 @@ Section fixpoint2_ne.
     (∀ x y, fA x y ≡ fA' x y) → (∀ x y, fB x y ≡ fB' x y) →
     fixpoint_B fA fB ≡ fixpoint_B fA' fB'.
   Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_B_ne. Qed.
-End fixpoint2_ne.
+End fixpointAB_ne.
 
 (** Function space *)
 (* We make [ofe_fun] a definition so that we can register it as a canonical
-- 
GitLab