From 309cf3d3d6fe57ba9c15c32872b42433596c7748 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sat, 22 Dec 2018 02:04:26 +0100
Subject: Make `Instance` without a body always open a proof.

---
 plugins/setoid_ring/Ncring_initial.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/setoid_ring/Ncring_initial.v')

diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v
index 1ca6227f25..aa0370b2ac 100644
--- a/plugins/setoid_ring/Ncring_initial.v
+++ b/plugins/setoid_ring/Ncring_initial.v
@@ -32,6 +32,7 @@ Lemma Zsth : Equivalence (@eq Z).
 Proof. exact Z.eq_equiv. Qed.
 
 Instance Zops:@Ring_ops Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp (@eq Z).
+Defined.
 
 Instance Zr: (@Ring _ _ _ _ _ _ _ _ Zops).
 Proof.
-- 
cgit v1.2.3