diff options
| author | Maxime Dénès | 2017-10-30 14:16:48 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-30 14:16:48 +0100 |
| commit | e1b1743fb6aaed042d5e6762ea76c3242593ab1d (patch) | |
| tree | f2c7a9504fe1a1a39a9015a771bf07eba1696ca8 /mathcomp/ssreflect/bigop.v | |
| parent | d5437703555329168288467dc1a94b1176e1776e (diff) | |
Fix obsolete vernacular syntax for locality.
It was emitting a deprecation warning and will soon be removed from Coq.
Diffstat (limited to 'mathcomp/ssreflect/bigop.v')
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index c5d2ef3..a517c8a 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1094,14 +1094,14 @@ Import Monoid.Theory. Variable R : Type. Variable idx : R. -Notation Local "1" := idx. +Local Notation "1" := idx. Section Plain. Variable op : Monoid.law 1. -Notation Local "*%M" := op (at level 0). -Notation Local "x * y" := (op x y). +Local Notation "*%M" := op (at level 0). +Local Notation "x * y" := (op x y). Lemma eq_big_idx_seq idx' I r (P : pred I) F : right_id idx' *%M -> has P r -> @@ -1226,8 +1226,8 @@ Section Abelian. Variable op : Monoid.com_law 1. -Notation Local "'*%M'" := op (at level 0). -Notation Local "x * y" := (op x y). +Local Notation "'*%M'" := op (at level 0). +Local Notation "x * y" := (op x y). Lemma eq_big_perm (I : eqType) r1 r2 (P : pred I) F : perm_eq r1 r2 -> @@ -1517,14 +1517,14 @@ Import Monoid.Theory. Variable R : Type. Variables zero one : R. -Notation Local "0" := zero. -Notation Local "1" := one. +Local Notation "0" := zero. +Local Notation "1" := one. Variable times : Monoid.mul_law 0. -Notation Local "*%M" := times (at level 0). -Notation Local "x * y" := (times x y). +Local Notation "*%M" := times (at level 0). +Local Notation "x * y" := (times x y). Variable plus : Monoid.add_law 0 *%M. -Notation Local "+%M" := plus (at level 0). -Notation Local "x + y" := (plus x y). +Local Notation "+%M" := plus (at level 0). +Local Notation "x + y" := (plus x y). Lemma big_distrl I r a (P : pred I) F : \big[+%M/0]_(i <- r | P i) F i * a = \big[+%M/0]_(i <- r | P i) (F i * a). |