diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-06 11:29:10 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-06 17:00:30 +0100 |
| commit | ca609f7ea0653a282a81e5d4f9392b1c05a03d8f (patch) | |
| tree | 36a3cf7a8032c5c4040732ae7ea4ef2d71250c4b /test-suite/success | |
| parent | 34de09e9a072a937f1510d69cad1204a53e007aa (diff) | |
Restoring clear_flag (thanks a lot to jonikelee to notice it).
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/destruct.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index c74bda2a9..f5848ffe0 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -377,6 +377,14 @@ intros. Fail destruct H. Abort. +(* Check keep option (bug #3791) *) + +Goal forall b:bool, True. +intro b. +destruct !b. +clear b. (* b has to be here *) +Abort. + (* Check clearing of names *) Inductive IND2 : nat -> Prop := CONSTR2 : forall y, y = y -> IND2 y. |