aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Cases.out
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-07-29 14:35:45 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-07-29 14:35:45 +0000
commit5a75a4d046c24a5c6c9e452f08f0fa8305c88226 (patch)
tree3a4466f1e335c79767cb79260f47f74dbe2afec2 /test-suite/output/Cases.out
parent8ffad6dc0ea972bd7354be76be9e4c6a633e3692 (diff)
Update test-suite output
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11294 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output/Cases.out')
-rw-r--r--test-suite/output/Cases.out2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 9d0d06580..995754a6b 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -21,7 +21,7 @@ Argument scopes are [nat_scope nat_scope _ _ _]
foo =
fix foo (A : Type) (l : list A) {struct l} : option A :=
match l with
- | nil => None (A:=A)
+ | nil => None
| x0 :: nil => Some x0
| x0 :: (_ :: _) as l0 => foo A l0
end