diff options
Diffstat (limited to 'test-suite/bugs/closed/4240.v')
| -rw-r--r-- | test-suite/bugs/closed/4240.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4240.v b/test-suite/bugs/closed/4240.v new file mode 100644 index 00000000..083c59fe --- /dev/null +++ b/test-suite/bugs/closed/4240.v @@ -0,0 +1,12 @@ +(* Check that closure of filter did not restrict the former evar filter *) + +Lemma foo (new : nat) : False. +evar (H1: nat). +set (H3 := 0). +assert (H3' := id H3). +evar (H5: nat). +clear H3. +assert (H5 = new). +unfold H5. +unfold H1. +exact (eq_refl new). |