diff options
| author | Gaëtan Gilbert | 2021-01-07 13:55:23 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-01-18 13:08:17 +0100 |
| commit | 4419a101a4f5a108be90cf4e420f0b6961e6caac (patch) | |
| tree | c3a3dcede7a5901685d28da3d540451e39c4b6f1 /theories/Numbers/Cyclic/Abstract | |
| parent | 58a4f645ee6d306cb824c2ac2dfa21e460b9692a (diff) | |
Support locality attributes for Hint Rewrite (including export)
We deprecate unspecified locality as was done for Hint.
Close #13724
Diffstat (limited to 'theories/Numbers/Cyclic/Abstract')
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/NZCyclic.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v index e3e8f532b3..374af6de63 100644 --- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -348,7 +348,7 @@ Local Notation "- x" := (ZnZ.opp x). Local Infix "*" := ZnZ.mul. Local Notation wB := (base ZnZ.digits). -Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_add ZnZ.spec_mul +Global Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_add ZnZ.spec_mul ZnZ.spec_opp ZnZ.spec_sub : cyclic. diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index 7c5b43096a..f74a78e876 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -51,7 +51,7 @@ Local Infix "+" := add. Local Infix "-" := sub. Local Infix "*" := mul. -Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_succ ZnZ.spec_pred +Global Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_succ ZnZ.spec_pred ZnZ.spec_add ZnZ.spec_mul ZnZ.spec_sub : cyclic. Ltac zify := unfold eq, zero, one, two, succ, pred, add, sub, mul in *; |