diff options
Diffstat (limited to 'mathcomp')
28 files changed, 58 insertions, 58 deletions
diff --git a/mathcomp/algebra/fraction.v b/mathcomp/algebra/fraction.v index 8cf811a..98eb9f1 100644 --- a/mathcomp/algebra/fraction.v +++ b/mathcomp/algebra/fraction.v @@ -16,8 +16,8 @@ Unset Strict Implicit. Unset Printing Implicit Defensive. Import GRing.Theory. -Open Local Scope ring_scope. -Open Local Scope quotient_scope. +Local Open Scope ring_scope. +Local Open Scope quotient_scope. Reserved Notation "{ 'ratio' T }" (at level 0, format "{ 'ratio' T }"). Reserved Notation "{ 'fraction' T }" (at level 0, format "{ 'fraction' T }"). diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 2aa117d..5f47691 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -147,7 +147,7 @@ Unset Printing Implicit Defensive. Import GroupScope. Import GRing.Theory. -Open Local Scope ring_scope. +Local Open Scope ring_scope. Reserved Notation "''M_' n" (at level 8, n at level 2, format "''M_' n"). Reserved Notation "''rV_' n" (at level 8, n at level 2, format "''rV_' n"). @@ -193,7 +193,7 @@ Reserved Notation "\tr A" (at level 10, A at level 8, format "\tr A"). Reserved Notation "\det A" (at level 10, A at level 8, format "\det A"). Reserved Notation "\adj A" (at level 10, A at level 8, format "\adj A"). -Notation Local simp := (Monoid.Theory.simpm, oppr0). +Local Notation simp := (Monoid.Theory.simpm, oppr0). (*****************************************************************************) (****************************Type Definition**********************************) diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index 3b3ca5d..da61dfb 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -135,7 +135,7 @@ Unset Printing Implicit Defensive. Import GroupScope. Import GRing.Theory. -Open Local Scope ring_scope. +Local Open Scope ring_scope. Reserved Notation "\rank A" (at level 10, A at level 8, format "\rank A"). Reserved Notation "A ^C" (at level 8, format "A ^C"). @@ -160,7 +160,7 @@ Notation "''A' [ F ]_ n" := 'A[F]_(n) Delimit Scope matrix_set_scope with MS. -Notation Local simp := (Monoid.Theory.simpm, oppr0). +Local Notation simp := (Monoid.Theory.simpm, oppr0). (*****************************************************************************) (******************** Rank and row-space theory ******************************) diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index 1301a94..eeece16 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -64,7 +64,7 @@ Unset Printing Implicit Defensive. Import GRing.Theory. Import Monoid.Theory. -Open Local Scope ring_scope. +Local Open Scope ring_scope. Import Pdiv.Idomain. (* Row vector <-> bounded degree polynomial bijection *) diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index 22caa4a..56493dd 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -101,7 +101,7 @@ Unset Strict Implicit. Unset Printing Implicit Defensive. Import GRing.Theory. -Open Local Scope ring_scope. +Local Open Scope ring_scope. Reserved Notation "{ 'poly' T }" (at level 0, format "{ 'poly' T }"). Reserved Notation "c %:P" (at level 2, format "c %:P"). diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index da6dc59..b7a9052 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -93,7 +93,7 @@ Require Import finfun tuple ssralg matrix mxalgebra zmodp. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Open Local Scope ring_scope. +Local Open Scope ring_scope. Reserved Notation "{ 'vspace' T }" (at level 0, format "{ 'vspace' T }"). Reserved Notation "''Hom' ( T , rT )" (at level 8, format "''Hom' ( T , rT )"). diff --git a/mathcomp/attic/amodule.v b/mathcomp/attic/amodule.v index f4f80d0..d74288c 100644 --- a/mathcomp/attic/amodule.v +++ b/mathcomp/attic/amodule.v @@ -23,7 +23,7 @@ Require Import zmodp matrix vector falgebra galgebra. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Open Local Scope ring_scope. +Local Open Scope ring_scope. Delimit Scope amodule_scope with aMS. diff --git a/mathcomp/attic/fib.v b/mathcomp/attic/fib.v index def96bb..fefa0d2 100644 --- a/mathcomp/attic/fib.v +++ b/mathcomp/attic/fib.v @@ -312,7 +312,7 @@ Qed. Section Matrix. -Open Local Scope ring_scope. +Local Open Scope ring_scope. Import GRing.Theory. Variable R: ringType. diff --git a/mathcomp/attic/forms.v b/mathcomp/attic/forms.v index 3ea6ab1..a1a987b 100644 --- a/mathcomp/attic/forms.v +++ b/mathcomp/attic/forms.v @@ -9,7 +9,7 @@ Require Import finfun tuple ssralg matrix zmodp vector. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Open Local Scope ring_scope. +Local Open Scope ring_scope. Import GRing.Theory. diff --git a/mathcomp/attic/galgebra.v b/mathcomp/attic/galgebra.v index 5e12b38..4902a47 100644 --- a/mathcomp/attic/galgebra.v +++ b/mathcomp/attic/galgebra.v @@ -18,7 +18,7 @@ Unset Printing Implicit Defensive. Reserved Notation "g %:FG" (at level 2, left associativity, format "g %:FG"). -Open Local Scope ring_scope. +Local Open Scope ring_scope. Import GRing.Theory. Section GroupAlgebraDef. @@ -42,7 +42,7 @@ Lemma galgE : forall f, GAlg (finfun f) =1 f. Proof. by move=> f i; rewrite /fun_of_galg ffunE. Qed. Definition injG (g : gT) := GAlg ([ffun k => (k == g)%:R]). -Notation Local "g %:FG" := (injG g). +Local Notation "g %:FG" := (injG g). Implicit Types v: galg. diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v index 58eccc2..23f5cba 100644 --- a/mathcomp/field/falgebra.v +++ b/mathcomp/field/falgebra.v @@ -79,7 +79,7 @@ Require Import div tuple finfun bigop ssralg finalg zmodp matrix vector poly. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Open Local Scope ring_scope. +Local Open Scope ring_scope. Reserved Notation "{ 'aspace' T }" (at level 0, format "{ 'aspace' T }"). Reserved Notation "<< U & vs >>" (at level 0, format "<< U & vs >>"). diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v index e8b8944..6178c01 100644 --- a/mathcomp/field/separable.v +++ b/mathcomp/field/separable.v @@ -34,7 +34,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Open Local Scope ring_scope. +Local Open Scope ring_scope. Import GRing.Theory. Section SeparablePoly. diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index 06a1806..9d7bcc8 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -1242,7 +1242,7 @@ Structure group_type : Type := Group { }. Definition group_of of phant gT : predArgType := group_type. -Notation Local groupT := (group_of (Phant gT)). +Local Notation groupT := (group_of (Phant gT)). Identity Coercion type_of_group : group_of >-> group_type. Canonical group_subType := Eval hnf in [subType for gval]. diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v index 4ee2bc8..94304c4 100644 --- a/mathcomp/fingroup/gproduct.v +++ b/mathcomp/fingroup/gproduct.v @@ -1337,7 +1337,7 @@ Hypothesis nHK : K \subset 'N(H). Hypothesis actf : {in H & K, morph_act 'J 'J fH fK}. Hypothesis eqfHK : {in H :&: K, fH =1 fK}. -Notation Local f := (pprodm nHK actf eqfHK). +Local Notation f := (pprodm nHK actf eqfHK). Lemma pprodmE x a : x \in H -> a \in K -> f (x * a) = fH x * fK a. Proof. diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v index 9f0a900..2a70706 100644 --- a/mathcomp/fingroup/morphism.v +++ b/mathcomp/fingroup/morphism.v @@ -1006,7 +1006,7 @@ Variables (G : {group gT}) (H : {group hT}). Variable f : {morphism G >-> hT}. Variable g : {morphism H >-> rT}. -Notation Local gof := (mfun g \o mfun f). +Local Notation gof := (mfun g \o mfun f). Lemma comp_morphM : {in f @*^-1 H &, {morph gof: x y / x * y}}. Proof. diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v index a306475..6d9abdc 100644 --- a/mathcomp/fingroup/perm.v +++ b/mathcomp/fingroup/perm.v @@ -87,8 +87,8 @@ Bind Scope group_scope with perm_of. Notation "''S_' n" := {perm 'I_n} (at level 8, n at level 2, format "''S_' n"). -Notation Local fun_of_perm_def := (fun T (u : perm_type T) => val u : T -> T). -Notation Local perm_def := (fun T f injf => Perm (@perm_proof T f injf)). +Local Notation fun_of_perm_def := (fun T (u : perm_type T) => val u : T -> T). +Local Notation perm_def := (fun T f injf => Perm (@perm_proof T f injf)). Module Type PermDefSig. Parameter fun_of_perm : forall T, perm_type T -> T -> T. diff --git a/mathcomp/odd_order/BGappendixAB.v b/mathcomp/odd_order/BGappendixAB.v index cb104f4..1dc4472 100644 --- a/mathcomp/odd_order/BGappendixAB.v +++ b/mathcomp/odd_order/BGappendixAB.v @@ -31,7 +31,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Open Local Scope ring_scope. +Local Open Scope ring_scope. Import GroupScope GRing.Theory. Section AppendixA. diff --git a/mathcomp/solvable/alt.v b/mathcomp/solvable/alt.v index f43c89a..baf4792 100644 --- a/mathcomp/solvable/alt.v +++ b/mathcomp/solvable/alt.v @@ -36,7 +36,7 @@ Definition Sym of phant T : {set {perm T}} := setT. Canonical Sym_group phT := Eval hnf in [group of Sym phT]. -Notation Local "'Sym_T" := (Sym (Phant T)) (at level 0). +Local Notation "'Sym_T" := (Sym (Phant T)) (at level 0). Canonical sign_morph := @Morphism _ _ 'Sym_T _ (in2W (@odd_permM _)). @@ -44,7 +44,7 @@ Definition Alt of phant T := 'ker (@odd_perm T). Canonical Alt_group phT := Eval hnf in [group of Alt phT]. -Notation Local "'Alt_T" := (Alt (Phant T)) (at level 0). +Local Notation "'Alt_T" := (Alt (Phant T)) (at level 0). Lemma Alt_even p : (p \in 'Alt_T) = ~~ p. Proof. by rewrite !inE /=; case: odd_perm. Qed. diff --git a/mathcomp/solvable/gseries.v b/mathcomp/solvable/gseries.v index fe83ada..772db33 100644 --- a/mathcomp/solvable/gseries.v +++ b/mathcomp/solvable/gseries.v @@ -42,7 +42,7 @@ Section GroupDefs. Variable gT : finGroupType. Implicit Types A B U V : {set gT}. -Notation Local groupT := (group_of (Phant gT)). +Local Notation groupT := (group_of (Phant gT)). Definition subnormal A B := (A \subset B) && (iter #|B| (fun N => generated (class_support A N)) B == A). 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). diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index e11fd9f..3e8230e 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -696,7 +696,7 @@ Section SubEqType. Variables (T : eqType) (P : pred T) (sT : subType P). -Notation Local ev_ax := (fun T v => @Equality.axiom T (fun x y => v x == v y)). +Local Notation ev_ax := (fun T v => @Equality.axiom T (fun x y => v x == v y)). Lemma val_eqP : ev_ax sT val. Proof. exact: inj_eqAxiom val_inj. Qed. Definition sub_eqMixin := EqMixin val_eqP. diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index feac3ab..a9899b7 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -151,9 +151,9 @@ Notation "A :!=: B" := (A != B :> {set _}) Notation "A :=P: B" := (A =P B :> {set _}) (at level 70, no associativity, only parsing) : set_scope. -Notation Local finset_def := (fun T P => @FinSet T (finfun P)). +Local Notation finset_def := (fun T P => @FinSet T (finfun P)). -Notation Local pred_of_set_def := (fun T (A : set_type T) => val A : _ -> _). +Local Notation pred_of_set_def := (fun T (A : set_type T) => val A : _ -> _). Module Type SetDefSig. Parameter finset : forall T : finType, pred T -> {set T}. @@ -1021,9 +1021,9 @@ End CartesianProd. Implicit Arguments setXP [x1 x2 fT1 fT2 A1 A2]. Prenex Implicits setXP. -Notation Local imset_def := +Local Notation imset_def := (fun (aT rT : finType) f mD => [set y in @image_mem aT rT f mD]). -Notation Local imset2_def := +Local Notation imset2_def := (fun (aT1 aT2 rT : finType) f (D1 : mem_pred aT1) (D2 : _ -> mem_pred aT2) => [set y in @image_mem _ rT (prod_curry f) (mem [pred u | D1 u.1 & D2 u.1 u.2])]). diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 215c69b..1171fcb 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -430,8 +430,8 @@ Notation "[ 'disjoint' A & B ]" := (disjoint (mem A) (mem B)) (at level 0, format "'[hv' [ 'disjoint' '/ ' A '/' & B ] ']'") : bool_scope. -Notation Local subset_type := (forall (T : finType) (A B : mem_pred T), bool). -Notation Local subset_def := (fun T A B => pred0b (predD A B)). +Local Notation subset_type := (forall (T : finType) (A B : mem_pred T), bool). +Local Notation subset_def := (fun T A B => pred0b (predD A B)). Module Type SubsetDefSig. Parameter subset : subset_type. Axiom subsetEdef : subset = subset_def. End SubsetDefSig. diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrbool.v b/mathcomp/ssreflect/plugin/v8.5/ssrbool.v index c5a881f..f81e16e 100644 --- a/mathcomp/ssreflect/plugin/v8.5/ssrbool.v +++ b/mathcomp/ssreflect/plugin/v8.5/ssrbool.v @@ -1506,17 +1506,17 @@ Proof. by move=> trR x y z Ryx Rzy; apply: trR Rzy Ryx. Qed. (* Property localization *) -Notation Local "{ 'all1' P }" := (forall x, P x : Prop) (at level 0). -Notation Local "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0). -Notation Local "{ 'all3' P }" := (forall x y z, P x y z: Prop) (at level 0). -Notation Local ph := (phantom _). +Local Notation "{ 'all1' P }" := (forall x, P x : Prop) (at level 0). +Local Notation "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0). +Local Notation "{ 'all3' P }" := (forall x y z, P x y z: Prop) (at level 0). +Local Notation ph := (phantom _). Section LocalProperties. Variables T1 T2 T3 : Type. Variables (d1 : mem_pred T1) (d2 : mem_pred T2) (d3 : mem_pred T3). -Notation Local ph := (phantom Prop). +Local Notation ph := (phantom Prop). Definition prop_for (x : T1) P & ph {all1 P} := P x. diff --git a/mathcomp/ssreflect/plugin/v8.6/ssrbool.v b/mathcomp/ssreflect/plugin/v8.6/ssrbool.v index c5a881f..f81e16e 100644 --- a/mathcomp/ssreflect/plugin/v8.6/ssrbool.v +++ b/mathcomp/ssreflect/plugin/v8.6/ssrbool.v @@ -1506,17 +1506,17 @@ Proof. by move=> trR x y z Ryx Rzy; apply: trR Rzy Ryx. Qed. (* Property localization *) -Notation Local "{ 'all1' P }" := (forall x, P x : Prop) (at level 0). -Notation Local "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0). -Notation Local "{ 'all3' P }" := (forall x y z, P x y z: Prop) (at level 0). -Notation Local ph := (phantom _). +Local Notation "{ 'all1' P }" := (forall x, P x : Prop) (at level 0). +Local Notation "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0). +Local Notation "{ 'all3' P }" := (forall x y z, P x y z: Prop) (at level 0). +Local Notation ph := (phantom _). Section LocalProperties. Variables T1 T2 T3 : Type. Variables (d1 : mem_pred T1) (d2 : mem_pred T2) (d3 : mem_pred T3). -Notation Local ph := (phantom Prop). +Local Notation ph := (phantom Prop). Definition prop_for (x : T1) P & ph {all1 P} := P x. diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index 5c6acce..41243ea 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -105,7 +105,7 @@ Definition pfactor p e := p ^ e. Definition cons_pfactor (p e : nat) pd := ifnz e ((p, e) :: pd) pd. -Notation Local "p ^? e :: pd" := (cons_pfactor p e pd) +Local Notation "p ^? e :: pd" := (cons_pfactor p e pd) (at level 30, e at level 30, pd at level 60) : nat_scope. Section prime_decomp. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 32f507d..9ff9f61 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -856,7 +856,7 @@ Implicit Arguments revK [[T]]. Section EqSeq. Variables (n0 : nat) (T : eqType) (x0 : T). -Notation Local nth := (nth x0). +Local Notation nth := (nth x0). Implicit Type s : seq T. Implicit Types x y z : T. diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 4b9523f..8c21ae4 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -1395,10 +1395,10 @@ Definition exp m n := if n is n'.+1 then mul_exp m n' m else 1. Notation "n ^ m" := (exp n m) : nat_scope. -Notation Local oddn := odd. +Local Notation oddn := odd. Fixpoint odd n := if n is n'.+2 then odd n' else eqn n 1. -Notation Local doublen := double. +Local Notation doublen := double. Definition double n := if n is n'.+1 then n' + n.+1 else 0. Notation "n .*2" := (double n) : nat_scope. @@ -1460,7 +1460,7 @@ Fixpoint nat_of_pos p0 := End Trec. -Coercion Local nat_of_pos : positive >-> nat. +Local Coercion nat_of_pos : positive >-> nat. Coercion nat_of_bin b := if b is Npos p then p : nat else 0. |