diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/change.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/success/change.v b/test-suite/success/change.v index 7bed7ecb1..f775f818a 100644 --- a/test-suite/success/change.v +++ b/test-suite/success/change.v @@ -38,3 +38,10 @@ Fail change True with (let (x,a) := ex_intro _ True (eq_refl True) in x). Fail change True with match ex_intro _ True (eq_refl True) with ex_intro x _ => x end. Abort. + +(* Check absence of loop in identity substitution (was failing up to + Sep 2014, see #3641) *) + +Goal True. +change ?x with x. +Abort. |