From 86b5233bffa21ebe54775f66b0c9354e6f8cee26 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tesla=20Zhang=E2=80=AE?= <ice1000kotlin@foxmail.com>
Date: Wed, 24 Jan 2024 14:57:56 -0500
Subject: [PATCH] Remove the bad constructor on coinductive types

---
 Cubical/Codata/Conat/Base.agda | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Cubical/Codata/Conat/Base.agda b/Cubical/Codata/Conat/Base.agda
index 93974fb4e0..fdb5ec5fa6 100644
--- a/Cubical/Codata/Conat/Base.agda
+++ b/Cubical/Codata/Conat/Base.agda
@@ -1,4 +1,4 @@
-{- Conatural numbers (Tesla Ice Zhang, Feb. 2019)
+{- Conatural numbers (Tesla Zhang, Feb. 2019)
 
 This file defines:
 
@@ -30,7 +30,6 @@ record Conat : Type₀
 Conat′ = Unit ⊎ Conat
 record Conat where
   coinductive
-  constructor conat′
   field force : Conat′
 open Conat public