From 9354722485c71ba6fbe6e6462eae98113aa830cc Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Thu, 20 Apr 2017 17:50:10 +0200
Subject: Fix nsatz not recognizing real literals.

---
 plugins/nsatz/Nsatz.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'plugins/nsatz')

diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v
index b11d15e5c..403f664e2 100644
--- a/plugins/nsatz/Nsatz.v
+++ b/plugins/nsatz/Nsatz.v
@@ -462,6 +462,11 @@ try (try apply Rsth;
 exact Rplus_opp_r.
 Defined.
 
+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).
+
 Lemma R_one_zero: 1%R <> 0%R.
 discrR.
 Qed.
-- 
cgit v1.2.3