diff options
| author | Pierre-Marie Pédrot | 2021-01-19 10:02:32 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-19 10:02:32 +0100 |
| commit | 326df6dc176f70b3192f463164c3a435ab187bed (patch) | |
| tree | 8721d463b0f41e5134e823c756b72a936c4df607 /theories/Numbers/Cyclic | |
| parent | f44e65e0d209fdada20998d661ad10a5e82a0d92 (diff) | |
| parent | 4419a101a4f5a108be90cf4e420f0b6961e6caac (diff) | |
Merge PR #13725: Support locality attributes for Hint Rewrite (including export)
Ack-by: Zimmi48
Ack-by: gares
Reviewed-by: ppedrot
Diffstat (limited to 'theories/Numbers/Cyclic')
| -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 *; |