diff options
Diffstat (limited to 'mathcomp/attic')
| -rw-r--r-- | mathcomp/attic/Makefile | 4 | ||||
| -rw-r--r-- | mathcomp/attic/amodule.v | 2 | ||||
| -rw-r--r-- | mathcomp/attic/fib.v | 2 | ||||
| -rw-r--r-- | mathcomp/attic/forms.v | 2 | ||||
| -rw-r--r-- | mathcomp/attic/galgebra.v | 4 |
5 files changed, 7 insertions, 7 deletions
diff --git a/mathcomp/attic/Makefile b/mathcomp/attic/Makefile index e872352..a58be7b 100644 --- a/mathcomp/attic/Makefile +++ b/mathcomp/attic/Makefile @@ -11,12 +11,12 @@ MAKEFLAGS+=-B %: $(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq - $(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \ + $(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \ -f Makefile.coq $* .PHONY: clean clean: - $(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \ + $(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \ -f Makefile.coq clean $(H)rm -f Makefile.coq 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. |