From 513e194656429b6a9142a3a34095cee2c6f8ee96 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 20 Aug 2016 10:25:37 +0200
Subject: Fixing an anomaly in printing a unification error message.

---
 test-suite/success/Case13.v | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index f14725a8ee..8f95484cfd 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -55,6 +55,14 @@ Check (fun x : I' 0 => match x with
                        | _ => 0
                        end).
 
+(* This one could eventually be solved, the "Fail" is just to ensure *)
+(* that it does not fail with an anomaly, as it did at some time *)
+Fail Check (fun x : I' 0 => match x return _ x with
+                       | C2' _ _ => 0
+                       | niln => 0
+                       | _ => 0
+                       end).
+
 (* Check insertion of coercions around matched subterm *)
 
 Parameter A:Set.
-- 
cgit v1.2.3