From 7678b4f90930264041b34e0f77916f07dcaf6aaa Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 6 Dec 2017 20:41:51 +0100
Subject: [PATCH] Typo.
---
theories/base_logic/upred.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index bfaf99b2d..82abe8a6d 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -29,7 +29,7 @@ Section cofe.
(* A good way of understanding this defintion of the uPred OFE is to
consider the OFE uPred0 of monotonous SProp predicates. That is,
- uPred0 is the OFE of non-expanding functions from M to SProp that
+ uPred0 is the OFE of non-expansive functions from M to SProp that
are monotonous with respect to CMRA inclusion. This notion of
monotonicity has to be stated in the SProp logic. It is exactly
uPred_mono.
--
GitLab