From fb1221c54f7821615d65cf8137f16833f3aea83d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 28 Mar 2018 10:29:29 +0200
Subject: [PATCH] Fix typos.

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

diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 3a4f1c92b..931b44cc6 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -37,9 +37,9 @@ Section proofs.
   Global Instance cinv_persistent N γ P : Persistent (cinv N γ P).
   Proof. rewrite /cinv; apply _. Qed.
 
-  Global Instance cinv_own_fractionnal γ : Fractional (cinv_own γ).
+  Global Instance cinv_own_fractional γ : Fractional (cinv_own γ).
   Proof. intros ??. by rewrite -own_op. Qed.
-  Global Instance cinv_own_as_fractionnal γ q :
+  Global Instance cinv_own_as_fractional γ q :
     AsFractional (cinv_own γ q) (cinv_own γ) q.
   Proof. split. done. apply _. Qed.
 
-- 
GitLab