From 993e6a0df37216908ea566361d1f5e527e82b1e1 Mon Sep 17 00:00:00 2001 From: Anton Trunov Date: Fri, 29 Dec 2017 16:21:14 +0100 Subject: Fix core hint database issue #6521 --- theories/Init/Peano.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'theories') 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. -- cgit v1.2.3