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).

1 files changed, 7 insertions, 0 deletions

diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index e42663505..49c465b6c 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.