diff options
| author | Pierre-Marie Pédrot | 2018-11-19 19:34:42 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-19 19:34:42 +0100 |
| commit | 22c0b10f139d9a30fcbe4a5a489022e2b94130e9 (patch) | |
| tree | f4b84d2114aa4523aebf62f020ae46f4321fb10a /theories/Numbers | |
| parent | ba8e3caa31e464d1007c4ad54e8d70fd70ca3300 (diff) | |
| parent | eeb1d861551e25c6a92721334b3c9f36b7ebb012 (diff) | |
Merge PR #8987: Deprecate hint declaration/removal with no specified database
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/Cyclic/ZModulo/ZModulo.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NDefOps.v | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index 784e81758c..4bcd22543f 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -60,7 +60,7 @@ Section ZModulo. apply Z.lt_gt. unfold wB, base; auto with zarith. Qed. - Hint Resolve wB_pos. + Hint Resolve wB_pos : core. Lemma spec_to_Z_1 : forall x, 0 <= [|x|]. Proof. @@ -71,7 +71,7 @@ Section ZModulo. Proof. unfold to_Z; intros; destruct (Z_mod_lt x wB wB_pos); auto. Qed. - Hint Resolve spec_to_Z_1 spec_to_Z_2. + Hint Resolve spec_to_Z_1 spec_to_Z_2 : core. Lemma spec_to_Z : forall x, 0 <= [|x|] < wB. Proof. @@ -732,7 +732,7 @@ Section ZModulo. Proof. induction p; simpl; auto with zarith. Qed. - Hint Resolve Ptail_pos. + Hint Resolve Ptail_pos : core. Lemma Ptail_bounded : forall p d, Zpos p < 2^(Zpos d) -> Ptail p < Zpos d. Proof. diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v index 8e1be0d702..4539dea276 100644 --- a/theories/Numbers/Natural/Abstract/NDefOps.v +++ b/theories/Numbers/Natural/Abstract/NDefOps.v @@ -383,7 +383,7 @@ f_equiv. apply E, half_decrease. rewrite two_succ, <- not_true_iff_false, ltb_lt, nlt_ge, le_succ_l in H. order'. Qed. -Hint Resolve log_good_step. +Hint Resolve log_good_step : core. Theorem log_init : forall n, n < 2 -> log n == 0. Proof. |