diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-26 11:45:38 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-26 11:45:38 +0200 |
| commit | 4013bf624048960ac43e6843af2c170a46031b31 (patch) | |
| tree | 0c0d26af29ef72011a2754eedf7ef0504eac8e74 | |
| parent | 041b8bc806f85114bc3b54101faa84996d6ab50b (diff) | |
Fix test-suite file for opened bug #1596
| -rw-r--r-- | test-suite/bugs/opened/1596.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/test-suite/bugs/opened/1596.v b/test-suite/bugs/opened/1596.v index cae0fa934..91cd09910 100644 --- a/test-suite/bugs/opened/1596.v +++ b/test-suite/bugs/opened/1596.v @@ -2,6 +2,8 @@ Require Import Relations. Require Import FSets. Require Import Arith. +Require Import Omega. +Unset Standard Proposition Elimination Names. Lemma Bool_elim_bool : forall (b:bool),b=true \/ b=false. destruct b;try tauto. @@ -253,7 +255,7 @@ n). induction m;simpl;intro. elim (Bool_elim_bool (H.mem (MessageSpi.MNam n,n0) h));intros. apply SynInc;apply H.mem_2;trivial. - + Fail rewrite H in H0. (* !! impossible here !! *) Abort. (* discriminate H0. |