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 73c8c5ef4..d5322d094 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -92,7 +92,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.