diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 21:34:46 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 21:34:46 +0100 |
| commit | 866bad4e9cdaa6ff4419840f8c9980f770873176 (patch) | |
| tree | 14fbdbbebd25a4739ded1dcb8570f343c4633333 /theories | |
| parent | 97498d79324b4890977f0a9077ea4a01bc9cacfe (diff) | |
| parent | 993e6a0df37216908ea566361d1f5e527e82b1e1 (diff) | |
Merge PR #6522: 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 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. |