Test case for previous commit.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11641 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 13 insertions, 0 deletions

diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 61f89d403..37ee71e95 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -33,3 +33,16 @@ Fixpoint foo (A:Type) (l:list A) : option A :=
   end.
 
 Print foo.
+
+(* Do not duplicate the matched term *)
+
+Axiom A : nat -> bool.
+
+Definition foo' :=
+  match A 0 with
+    | true => true
+    | x => x
+  end.
+
+Print foo'.
+