diff options
| -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. |