diff options
Diffstat (limited to 'test-suite/success/destruct.v')
| -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. |