aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-12-09 12:24:39 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-12-09 12:24:39 +0000
commit0ca3c38f67809c87ee1caf3a3aa541816f79d3cc (patch)
tree7ee85cbab10b49b10672355338c4e1e9c2291823 /test-suite
parentdf848afcfaf69a7b132dea824f0cd1602898ea60 (diff)
Désactivation du test du printer arithmétique v7
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6442 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/output/Arith.out4
-rw-r--r--test-suite/output/Arith.v2
2 files changed, 0 insertions, 6 deletions
diff --git a/test-suite/output/Arith.out b/test-suite/output/Arith.out
deleted file mode 100644
index 210dd6ad3..000000000
--- a/test-suite/output/Arith.out
+++ /dev/null
@@ -1,4 +0,0 @@
-[n:nat](S (S n))
- : nat->nat
-[n:nat](S (plus n n))
- : nat->nat
diff --git a/test-suite/output/Arith.v b/test-suite/output/Arith.v
deleted file mode 100644
index 39989dfc3..000000000
--- a/test-suite/output/Arith.v
+++ /dev/null
@@ -1,2 +0,0 @@
-Check [n](S (S n)).
-Check [n](S (plus n n)).