diff options
author | 2015-04-10 16:14:09 +0200 | |
---|---|---|
committer | 2015-04-10 16:14:09 +0200 | |
commit | 07d63e1333dc73eda3e49e904ff8df6e7f62fa79 (patch) | |
tree | fad7851b41d628895b717d8915ae9c1a7d5f271a /test-suite/bugs/closed/3199.v | |
parent | 9cd8bbc7808479c71e4413bc6f3555f494feda09 (diff) |
Test for bug #3199.
Diffstat (limited to 'test-suite/bugs/closed/3199.v')
-rw-r--r-- | test-suite/bugs/closed/3199.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3199.v b/test-suite/bugs/closed/3199.v new file mode 100644 index 000000000..08bf62493 --- /dev/null +++ b/test-suite/bugs/closed/3199.v @@ -0,0 +1,18 @@ +Axiom P : nat -> Prop. +Axiom admit : forall n : nat, P n -> P n -> n = S n. +Axiom foo : forall n, P n. + +Create HintDb bar. +Hint Extern 3 => symmetry : bar. +Hint Resolve admit : bar. +Hint Immediate foo : bar. + +Lemma qux : forall n : nat, n = S n. +Proof. +intros n. +eauto with bar. +Defined. + +Goal True. +pose (e := eq_refl (qux 0)); unfold qux in e. +match type of e with context [eq_sym] => fail 1 | _ => idtac end. |