1 files changed, 4 insertions, 1 deletions
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index 7c2b7c0b..499c0660 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -10,6 +10,10 @@ Type match 0, eq, 0 return nat with
      | O, x, y => 0
      | S x, y, z => x
      end.
+Type match 0, eq, 0 return _ with
+     | O, x, y => 0
+     | S x, y, z => x
+     end.
 
 (* Non dependent form of annotation *)
 Type match 0, eq return nat with
@@ -406,7 +410,6 @@ Type match niln with
      | x => 0
      end.
 
-
 Type match niln return nat with
      | niln => 0
      | consn n a l => a