From 8fb17c4cac1336e17fd8b95aadb456e2b292657f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 19 Dec 2001 22:42:08 +0000
Subject: Test sobriété de la réduction de Intuition

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2350 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/output/Intuition.out | 7 +++++++
 test-suite/output/Intuition.v   | 3 +++
 2 files changed, 10 insertions(+)
 create mode 100644 test-suite/output/Intuition.out
 create mode 100644 test-suite/output/Intuition.v

diff --git a/test-suite/output/Intuition.out b/test-suite/output/Intuition.out
new file mode 100644
index 0000000000..cadb35c630
--- /dev/null
+++ b/test-suite/output/Intuition.out
@@ -0,0 +1,7 @@
+1 subgoal
+  
+  m : Z
+  n : Z
+  H : `m >= n`
+  ============================
+   `m >= m`
diff --git a/test-suite/output/Intuition.v b/test-suite/output/Intuition.v
new file mode 100644
index 0000000000..94b5785e8f
--- /dev/null
+++ b/test-suite/output/Intuition.v
@@ -0,0 +1,3 @@
+Require ZArith.
+Goal (m,n:Z) `m >= n` -> `m >= m` /\ `m >= n`.
+Intros; Intuition.
-- 
cgit v1.2.3