diff options
| author | Hugo Herbelin | 2014-12-15 16:48:32 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-15 19:18:42 +0100 |
| commit | c73f114a46d50ab7c22218db0e80d5da96a824e4 (patch) | |
| tree | bb25f7c078face1ef8a9b228f234773b3d1243b1 /theories/Numbers/Cyclic/Abstract | |
| parent | a87dd193cb6a31ba528626e34a1bbb9b58c14f2e (diff) | |
Failing on unbound notation variable in notation level modifiers
+ consequences of this check on the standard library (moved the no-op
in Notation modifiers to what there were supposed to do; these are
anyway local notations, so compatibility is safe - please AS or PL,
amend if needed).
Diffstat (limited to 'theories/Numbers/Cyclic/Abstract')
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v index 3586cb7f21..2a9f07b0a5 100644 --- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -102,10 +102,10 @@ Module ZnZ. Let wB := base digits. Notation "[+| c |]" := - (interp_carry 1 wB to_Z c) (at level 0, x at level 99). + (interp_carry 1 wB to_Z c) (at level 0, c at level 99). Notation "[-| c |]" := - (interp_carry (-1) wB to_Z c) (at level 0, x at level 99). + (interp_carry (-1) wB to_Z c) (at level 0, c at level 99). Notation "[|| x ||]" := (zn2z_to_Z wB to_Z x) (at level 0, x at level 99). |