aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Intuition.out
diff options
context:
space:
mode:
authorGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-07-23 11:28:23 +0000
committerGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-07-23 11:28:23 +0000
commit7c63540ea9ed995599aee1f835e4865c141a58b0 (patch)
tree741bf05de3453f3a0fb41eca7a09ea4d02750caa /test-suite/output/Intuition.out
parent37c2da550906bda26b696ac5a1130dcc5dee6fba (diff)
removed thesis
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10040 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output/Intuition.out')
-rw-r--r--test-suite/output/Intuition.out1
1 files changed, 0 insertions, 1 deletions
diff --git a/test-suite/output/Intuition.out b/test-suite/output/Intuition.out
index 283d87d54..5831c9f43 100644
--- a/test-suite/output/Intuition.out
+++ b/test-suite/output/Intuition.out
@@ -4,5 +4,4 @@
n : Z
H : (m >= n)%Z
============================
- thesis :=
(m >= m)%Z