summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/2136.v
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:43:16 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:43:16 +0100
commitf219abfed720305c13875c3c63f9240cf63f78bc (patch)
tree69d2c026916128fdb50b8d1c0dbf1be451340d30 /test-suite/bugs/closed/2136.v
parent476d60ef0fe0ac015c1e902204cdd7029e10ef0f (diff)
parentcec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff)
Merge tag 'upstream/8.5_beta1+dfsg'
Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/bugs/closed/2136.v')
-rw-r--r--test-suite/bugs/closed/2136.v61
1 files changed, 61 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2136.v b/test-suite/bugs/closed/2136.v
new file mode 100644
index 00000000..d2b926f3
--- /dev/null
+++ b/test-suite/bugs/closed/2136.v
@@ -0,0 +1,61 @@
+(* Bug #2136
+
+The fsetdec tactic seems to get confused by hypotheses like
+ HeqH1 : H1 = MkEquality s0 s1 b
+If I clear them then it is able to solve my goal; otherwise it is not.
+I would expect it to be able to solve the goal even without this hypothesis
+being cleared. A small, self-contained example is below.
+
+I have coq r12238.
+
+
+Thanks
+Ian
+*)
+
+
+Require Import FSets.
+Require Import Arith.
+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 Dec := WDecide (NatSet).
+Import FSetDecideAuxiliary.
+
+Parameter MkEquality : forall ( s0 s1 : NatSet.t )
+ ( x : nat ),
+ NatSet.Equal s1 (NatSet.add x s0).
+
+Lemma ThisLemmaWorks : forall ( s0 s1 : NatSet.t )
+ ( a b : nat ),
+ NatSet.In a s0
+ -> NatSet.In a s1.
+Proof.
+intros.
+remember (MkEquality s0 s1 b) as H1.
+clear HeqH1.
+fsetdec.
+Qed.
+
+Lemma ThisLemmaWasFailing : forall ( s0 s1 : NatSet.t )
+ ( a b : nat ),
+ NatSet.In a s0
+ -> NatSet.In a s1.
+Proof.
+intros.
+remember (MkEquality s0 s1 b) as H1.
+fsetdec.
+(*
+Error: Tactic failure: because the goal is beyond the scope of this tactic.
+*)
+Qed. \ No newline at end of file