1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 61f89d40..37ee71e9 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'.
+