diff options
author | 2010-06-18 16:19:49 +0000 | |
---|---|---|
committer | 2010-06-18 16:19:49 +0000 | |
commit | 5818c354fff1671fac26345ed9d6300ac25efcb2 (patch) | |
tree | 1834ffa1bf71bb9c5c06a49f85d2a87971812b61 /test-suite/bugs/closed/shouldsucceed/2281.v | |
parent | 726c669428f1cd1f69fa8f73e0c97b34169ff665 (diff) |
add in test-suite the scripts about fsetdec bugs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13165 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/2281.v')
-rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2281.v | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2281.v b/test-suite/bugs/closed/shouldsucceed/2281.v new file mode 100644 index 000000000..40948d905 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2281.v @@ -0,0 +1,50 @@ +(** Bug #2281 + +In the code below, coq is confused by an equality unless it is first 'subst'ed +away, yet http://coq.inria.fr/stdlib/Coq.FSets.FSetDecide.html says + + fsetdec will first perform any necessary zeta and beta reductions and will +invoke subst to eliminate any Coq equalities between finite sets or their +elements. + +I have coq r12851. + +*) + +Require Import Arith. +Require Import FSets. +Require Import FSetWeakList. + +Module DecidableNat. +Definition t := nat. +Definition eq := @eq nat. +Definition eq_refl := @refl_equal nat. +Definition eq_sym := @sym_eq nat. +Definition eq_trans := @trans_eq nat. +Definition eq_dec := eq_nat_dec. +End DecidableNat. + +Module NatSet := Make(DecidableNat). + +Module Export NameSetDec := WDecide (NatSet). + +Lemma ThisLemmaWorks : forall ( s1 s2 : NatSet.t ) + ( H : s1 = s2 ), + NatSet.Equal s1 s2. +Proof. +intros. +subst. +fsetdec. +Qed. + +Import FSetDecideAuxiliary. + +Lemma ThisLemmaWasFailing : forall ( s1 s2 : NatSet.t ) + ( H : s1 = s2 ), + NatSet.Equal s1 s2. +Proof. +intros. +fsetdec. +(* Error: Tactic failure: because the goal is beyond the scope of this tactic. +*) +Qed.
\ No newline at end of file |