From 8a89173127428a02a30ed8ffa9b8083ef0ce757a Mon Sep 17 00:00:00 2001
From: mohring
Date: Fri, 13 Apr 2001 05:23:38 +0000
Subject: ajout de tests

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

diff --git a/test-suite/failure/check.v b/test-suite/failure/check.v
new file mode 100644
index 0000000000..77f2252b88
--- /dev/null
+++ b/test-suite/failure/check.v
@@ -0,0 +1,3 @@
+Implicits eq [1].
+
+Check (eq bool).
\ No newline at end of file
diff --git a/test-suite/failure/params_ind.v b/test-suite/failure/params_ind.v
new file mode 100644
index 0000000000..206891286a
--- /dev/null
+++ b/test-suite/failure/params_ind.v
@@ -0,0 +1,4 @@
+Inductive list [A:Set] : Set :=
+   nil : (list A)
+|  cons : A -> (list A->A)-> (list A).
+
-- 
cgit v1.2.3