diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-07-16 20:21:58 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-07-16 20:24:31 +0200 |
| commit | 8591217a89f0b71e8175752dc55c42a5b89fccec (patch) | |
| tree | 1bac3968b932b461cea285d4141136493408bb41 /test-suite/bugs/closed/4240.v | |
| parent | 6a15394c542e5f16bce9b75fc033397c454f47e9 (diff) | |
Fixing bug #4240 (closure_of_filter was not ensuring refinement of
former filter after 48509b61 and 3cd718c, because filtered let-ins
were not any longer preserved).
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 000000000..083c59fe6 --- /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). |