2 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 995754a6b..1f0e12d3f 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 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'.
+