Test case for previous commit.

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

2 files changed, 15 insertions, 0 deletions

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 995754a6b1..1f0e12d3f7 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -28,3 +28,5 @@ fix foo (A : Type) (l : list A) {struct l} : option A :=
      : forall A : Type, list A -> option A
 
 Argument scopes are [type_scope list_scope]
+foo' = if A 0 then true else false
+     : bool
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 61f89d403a..37ee71e957 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'.
+