From 436f4abe0d06a75bdb1a0c28702d48d23e41f044 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 6 Feb 2020 14:50:40 +0100
Subject: [PATCH] cancellable -> cancelable

---
 theories/bi/lib/counterexamples.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/bi/lib/counterexamples.v b/theories/bi/lib/counterexamples.v
index 3c4467d8b..029e1cffc 100644
--- a/theories/bi/lib/counterexamples.v
+++ b/theories/bi/lib/counterexamples.v
@@ -234,7 +234,7 @@ Module linear1. Section linear1.
   Hypothesis fupd_fupd : ∀ E1 E2 E3 P, fupd E1 E2 (fupd E2 E3 P) ⊢ fupd E1 E3 P.
   Hypothesis fupd_frame_l : ∀ E1 E2 P Q, P ∗ fupd E1 E2 Q ⊢ fupd E1 E2 (P ∗ Q).
 
-  (** We have cancellable invariants. (Really they would have fractions at
+  (** We have cancelable invariants. (Really they would have fractions at
   [cinv_own] but we do not need that. They would also have a name matching
   the [mask] type, but we do not need that either.) *)
   Context (gname : Type) (cinv : gname → PROP → PROP) (cinv_own : gname → PROP).
@@ -288,7 +288,7 @@ Module linear2. Section linear2.
   Hypothesis fupd_fupd : ∀ E1 E2 E3 P, fupd E1 E2 (fupd E2 E3 P) ⊢ fupd E1 E3 P.
   Hypothesis fupd_frame_l : ∀ E1 E2 P Q, P ∗ fupd E1 E2 Q ⊢ fupd E1 E2 (P ∗ Q).
 
-  (** We have cancellable invariants. (Really they would have fractions at
+  (** We have cancelable invariants. (Really they would have fractions at
   [cinv_own] but we do not need that. They would also have a name matching
   the [mask] type, but we do not need that either.) *)
   Context (gname : Type) (cinv : gname → PROP → PROP) (cinv_own : gname → PROP).
-- 
GitLab