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/nsatz/Nsatz.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'plugins/nsatz')

diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v
index c5a09d677e..a964febf9c 100644
--- a/plugins/nsatz/Nsatz.v
+++ b/plugins/nsatz/Nsatz.v
@@ -452,6 +452,7 @@ constructor;red;intros;subst;trivial.
 Qed.
 
 Instance Rops: (@Ring_ops R 0%R 1%R Rplus Rmult Rminus Ropp (@eq R)).
+Defined.
 
 Instance Rri : (Ring (Ro:=Rops)).
 constructor;
@@ -468,6 +469,7 @@ Class can_compute_Z (z : Z) := dummy_can_compute_Z : True.
 Hint Extern 0 (can_compute_Z ?v) =>
   match isZcst v with true => exact I end : typeclass_instances.
 Instance reify_IZR z lvar {_ : can_compute_Z z} : reify (PEc z) lvar (IZR z).
+Defined.
 
 Lemma R_one_zero: 1%R <> 0%R.
 discrR.
@@ -484,6 +486,7 @@ exact Rmult_integral. exact R_one_zero. Defined.
 Require Import QArith.
 
 Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq).
+Defined.
 
 Instance Qri : (Ring (Ro:=Qops)).
 constructor.
-- 
cgit v1.2.3