diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-19 10:23:46 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-19 10:38:43 +0200 |
| commit | 0d90ab680abd1f558f1c20b79b66ca6b71864fbf (patch) | |
| tree | 5fa2cb4c3770ecd802b85cfa9c82c54508d6915a /test-suite/success/change.v | |
| parent | 07e4438bd758c2ced8caf09a6961ccd77d84e42b (diff) | |
Fixing #3641 (loop in e_contextually, introduced in r16525).
Diffstat (limited to 'test-suite/success/change.v')
| -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. |