From ee02c17a2e8a10c4f6f6b47e8875f2f9b1a3d42f Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 25 Jan 2019 13:01:21 +0000
Subject: [stdlib] Do not put INR_eq in the “real” hint database

---
 test-suite/output/NoAxiomFromR.out |  1 +
 test-suite/output/NoAxiomFromR.v   | 10 ++++++++++
 2 files changed, 11 insertions(+)
 create mode 100644 test-suite/output/NoAxiomFromR.out
 create mode 100644 test-suite/output/NoAxiomFromR.v

(limited to 'test-suite')

diff --git a/test-suite/output/NoAxiomFromR.out b/test-suite/output/NoAxiomFromR.out
new file mode 100644
index 0000000000..7d7c521343
--- /dev/null
+++ b/test-suite/output/NoAxiomFromR.out
@@ -0,0 +1 @@
+Closed under the global context
diff --git a/test-suite/output/NoAxiomFromR.v b/test-suite/output/NoAxiomFromR.v
new file mode 100644
index 0000000000..9cf6879699
--- /dev/null
+++ b/test-suite/output/NoAxiomFromR.v
@@ -0,0 +1,10 @@
+Require Import Psatz.
+
+Inductive TT : Set :=
+| C : nat -> TT.
+
+Lemma lem4 : forall (n m : nat),
+S m <= m -> C (S m) <> C n -> False.
+Proof. firstorder. Qed.
+
+Print Assumptions lem4.
-- 
cgit v1.2.3