aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure
diff options
context:
space:
mode:
authorGravatar mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-11-03 07:13:46 +0000
committerGravatar mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-11-03 07:13:46 +0000
commit0f9cf95f65bb0ccde65a8df7a620eecf6ca7f6e9 (patch)
tree3f493160eb485637f0ac719229080daa836e30e6 /test-suite/failure
parentd3db2fe245f7d79fe646d36943e7968d2a1073c9 (diff)
deplacement params_ind
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7497 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/failure')
-rw-r--r--test-suite/failure/params_ind.v4
1 files changed, 0 insertions, 4 deletions
diff --git a/test-suite/failure/params_ind.v b/test-suite/failure/params_ind.v
deleted file mode 100644
index 206891286..000000000
--- a/test-suite/failure/params_ind.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Inductive list [A:Set] : Set :=
- nil : (list A)
-| cons : A -> (list A->A)-> (list A).
-