From 2fedcccb35c2d18600cfaf89868fddd47564c982 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 16 Jul 2022 12:50:02 -0400
Subject: [PATCH] fix a comment

---
 theories/typing/type.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/typing/type.v b/theories/typing/type.v
index f197ac81..445d063c 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -290,7 +290,7 @@ Section type_dist2.
   Proof. destruct n as [|n]; first by split. apply type_dist2_equivalence. Qed.
 
   (* The hierarchy of metrics:
-     dist n → type_dist2 n → dist_later n → type_dist2_later. *)
+     dist n → type_dist2 n → dist_later n → type_dist2_later n. *)
   Lemma type_dist_dist2 n ty1 ty2 : dist n ty1 ty2 → type_dist2 n ty1 ty2.
   Proof. intros EQ. split; intros; try apply dist_dist_later; apply EQ. Qed.
   Lemma type_dist2_dist_later n ty1 ty2 : type_dist2 n ty1 ty2 → dist_later n ty1 ty2.
-- 
GitLab