From 462cd86ca8c27d4ef471f6f2e305089c442bac34 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Thu, 16 May 2019 23:04:26 +0200
Subject: [PATCH] Fix typo
---
theories/algebra/ofe.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 1568c9917..8f7f0b84a 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -11,7 +11,7 @@ Set Primitive Projections.
cases, we do not even need non-expansiveness.
*)
-(** Unbundeled version *)
+(** Unbundled version *)
Class Dist A := dist : nat → relation A.
Instance: Params (@dist) 3 := {}.
Notation "x ≡{ n }≡ y" := (dist n x y)
@@ -43,7 +43,7 @@ Record OfeMixin A `{Equiv A, Dist A} := {
mixin_dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y
}.
-(** Bundeled version *)
+(** Bundled version *)
Structure ofeT := OfeT {
ofe_car :> Type;
ofe_equiv : Equiv ofe_car;
--
GitLab