Fixing an interpretation bug of the "in" clause of "match".

- The head of "in" was wrongly considered binding
- Aliases in the "in" pattern were not taken into account

1 files changed, 9 insertions, 0 deletions

diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index 52fe98ac07..232ac17cbf 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -1873,3 +1873,12 @@ Check match niln in listn O return O=O with niln => eq_refl end.
 (* (was failing up to May 2017) *)
 
 Check fun x => match x with (y,z) as t as w => (y+z,t) = (0,w) end.
+
+(* A test about binding variables of "in" clause of "match" *)
+(* (was failing from 8.5 to Dec 2018) *)
+
+Check match O in nat return nat with O => O | _ => O end.
+
+(* Checking that aliases are substituted in the correct order *)
+
+Check match eq_refl (1,0) in _ = (y as z, y' as z) return z = z with eq_refl => eq_refl end : 0=0.