aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init/Peano.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Init/Peano.v')
-rw-r--r--theories/Init/Peano.v4
1 files changed, 3 insertions, 1 deletions
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 571d2f2dd..1316b8624 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -90,7 +90,9 @@ Lemma plus_n_O : forall n:nat, n = n + 0.
Proof.
induction n; simpl; auto.
Qed.
-Hint Resolve plus_n_O: core.
+
+Remove Hints eq_refl : core.
+Hint Resolve plus_n_O eq_refl: core. (* We want eq_refl to have higher priority than plus_n_O *)
Lemma plus_O_n : forall n:nat, 0 + n = n.
Proof.