From e845e9ad361a2766752f59d161eca2533f486bc8 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Fri, 8 Dec 2023 17:25:25 +0900
Subject: [PATCH] fix

---
 theories/nsatz_realtype.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/nsatz_realtype.v b/theories/nsatz_realtype.v
index a91866301c..767ece169f 100644
--- a/theories/nsatz_realtype.v
+++ b/theories/nsatz_realtype.v
@@ -39,6 +39,7 @@ Instance Nsatz_realType_Ring_ops:
   Nsatz_realType_mul
   Nsatz_realType_sub
   Nsatz_realType_opp (@eq T)).
+Proof.
 Defined.
 
 #[global]