diff options
| author |  Anton Trunov <anton.trunov@imdea.org> | 2017-12-29 16:21:14 +0100 |
|---|---|---|
| committer | Anton Trunov <anton.trunov@imdea.org> | 2018-01-03 12:08:41 +0100 |
| commit | 993e6a0df37216908ea566361d1f5e527e82b1e1 (patch) | |
| tree | 126df256db59d9f3e2b606cf8de8be64a98f7792 /theories | |
| parent | 7e319ad03aba413f3165b848eaf821b364f9291b (diff) | |
Fix core hint database issue #6521
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Init/Peano.v | 4 |
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. |