From 2d568a895d5c8a246f497c94c79811d3aad4269f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 Jan 2016 00:20:46 +0100
Subject: Fixing #4467 (continued).

Function is_constructor was not properly fixed. Additionally, this fixes
a problem with the 8.5 interpretation of in-pattern (see Cases.v).
---
 test-suite/success/Cases.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index e42663505d..49c465b6c6 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -1861,3 +1861,10 @@ Type (fun n => match n with
 
 Definition transport {A} (P : A->Type) {x y : A} (p : x=y) (u : P x) : P y :=
   match p with eq_refl => u end.
+
+(* Check in-pattern clauses with constant constructors, which were
+   previously interpreted as variables (before 8.5) *)
+
+Check match eq_refl 0 in _=O return O=O with eq_refl => eq_refl end.
+
+Check match niln in listn O return O=O with niln => eq_refl end.
-- 
cgit v1.2.3