diff options
Diffstat (limited to 'test-suite/bugs/opened/1596.v')
| -rw-r--r-- | test-suite/bugs/opened/1596.v | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/test-suite/bugs/opened/1596.v b/test-suite/bugs/opened/1596.v index 91cd09910..7c5dc4167 100644 --- a/test-suite/bugs/opened/1596.v +++ b/test-suite/bugs/opened/1596.v @@ -1,10 +1,11 @@ - Require Import Relations. Require Import FSets. Require Import Arith. Require Import Omega. Unset Standard Proposition Elimination Names. +Set Keyed Unification. + Lemma Bool_elim_bool : forall (b:bool),b=true \/ b=false. destruct b;try tauto. Qed. @@ -255,9 +256,6 @@ 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. - Qed.*) + rewrite H in H0. discriminate. (* !! impossible here !! *) + Qed. End B.
\ No newline at end of file |