From 7dd1b9af383707363272524dd7f0b1e6be9df6b3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 3 Sep 2020 10:21:09 +0200
Subject: [PATCH] Type annotations.

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

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 640045978..c54e539c3 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -38,9 +38,9 @@ Tactic Notation "ofe_subst" :=
   end.
 
 Record OfeMixin A `{Equiv A, Dist A} := {
-  mixin_equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y;
-  mixin_dist_equivalence n : Equivalence (dist n);
-  mixin_dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y
+  mixin_equiv_dist (x y : A) : x ≡ y ↔ ∀ n, x ≡{n}≡ y;
+  mixin_dist_equivalence n : Equivalence (@dist A _ n);
+  mixin_dist_S n (x y : A) : x ≡{S n}≡ y → x ≡{n}≡ y
 }.
 
 (** Bundled version *)
-- 
GitLab