diff options
99 files changed, 115 insertions, 115 deletions
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 5ce5e0436..db4a5d3cd 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -1028,7 +1028,7 @@ You can use a what is called a hints' base. \begin{coq_example} Require Import ZArith. Require Ring. -Open Local Scope Z_scope. +Local Open Scope Z_scope. Lemma toto1 : 1+1 = 2. ring. Qed. @@ -1124,7 +1124,7 @@ Just use the {\ring} tactic. \begin{coq_example} Require Import ZArith. Require Ring. -Open Local Scope Z_scope. +Local Open Scope Z_scope. Goal forall a b : Z, (a+b)*(a+b) = a*a + 2*a*b + b*b. intros. ring. @@ -1138,7 +1138,7 @@ Just use the {\field} tactic. \begin{coq_example} Require Import Reals. Require Ring. -Open Local Scope R_scope. +Local Open Scope R_scope. Goal forall a b : R, b*a<>0 -> (a/b) * (b/a) = 1. intros. field. @@ -1157,7 +1157,7 @@ Qed. \begin{coq_example} Require Import ZArith. Require Omega. -Open Local Scope Z_scope. +Local Open Scope Z_scope. Goal forall a : Z, a>0 -> a+a > a. intros. omega. @@ -1310,7 +1310,7 @@ You need to use the {\try} and {\solve} tactics. For instance: \begin{coq_example} Require Import ZArith. Require Ring. -Open Local Scope Z_scope. +Local Open Scope Z_scope. Goal forall a b c : Z, a+b=b+a. Proof with try solve [ring]. intros... diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index ff85b629b..465ee925e 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -4091,7 +4091,7 @@ the tactic. No database name is given: the hint is registered in the {\tt core} database. -\item\texttt{Hint Local} \textsl{hint\_definition} \texttt{:} +\item\texttt{Local Hint} \textsl{hint\_definition} \texttt{:} \ident$_1$ \ldots\ \ident$_n$ This is used to declare hints that must not be exported to the other @@ -4099,7 +4099,7 @@ the tactic. section, the option {\tt Local} is useless since hints do not survive anyway to the closure of sections. -\item\texttt{Hint Local} \textsl{hint\_definition} +\item\texttt{Local Hint} \textsl{hint\_definition} Idem for the {\tt core} database. diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index bc08deaf9..cc6a7066a 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -8,7 +8,7 @@ Require Import Arith Max Min BinInt BinNat Znat Nnat. -Open Local Scope Z_scope. +Local Open Scope Z_scope. (** * zify: the Z-ification tactic *) diff --git a/plugins/ring/LegacyArithRing.v b/plugins/ring/LegacyArithRing.v index fd5bcd935..94dc48a73 100644 --- a/plugins/ring/LegacyArithRing.v +++ b/plugins/ring/LegacyArithRing.v @@ -13,7 +13,7 @@ Require Export LegacyRing. Require Export Arith. Require Import Eqdep_dec. -Open Local Scope nat_scope. +Local Open Scope nat_scope. Fixpoint nateq (n m:nat) {struct m} : bool := match n, m with diff --git a/plugins/setoid_ring/RealField.v b/plugins/setoid_ring/RealField.v index 14c4270f9..1cbddc27d 100644 --- a/plugins/setoid_ring/RealField.v +++ b/plugins/setoid_ring/RealField.v @@ -5,7 +5,7 @@ Require Import Rdefinitions. Require Import Rpow_def. Require Import Raxioms. -Open Local Scope R_scope. +Local Open Scope R_scope. Lemma RTheory : ring_theory 0 1 Rplus Rmult Rminus Ropp (eq (A:=R)). Proof. diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v index 28ab33af3..681c4716b 100644 --- a/test-suite/success/ProgramWf.v +++ b/test-suite/success/ProgramWf.v @@ -25,7 +25,7 @@ Print merge. Print Z.lt. Print Zwf. -Open Local Scope Z_scope. +Local Open Scope Z_scope. Program Fixpoint Zwfrec (n m : Z) {measure (n + m) (Zwf 0)} : Z := match n ?= m with diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index 79d12a061..12ddbda84 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -68,7 +68,7 @@ where " Γ ⊢ τ " := (term Γ τ) : type_scope. Hint Constructors term : lambda. -Open Local Scope context_scope. +Local Open Scope context_scope. Ltac eqns := subst ; reverse ; simplify_dep_elim ; simplify_IH_hyps. diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index dd514653b..67039072b 100644 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v @@ -9,7 +9,7 @@ Require Import Le. Require Import Lt. -Open Local Scope nat_scope. +Local Open Scope nat_scope. Implicit Types k l p q r : nat. diff --git a/theories/Arith/Bool_nat.v b/theories/Arith/Bool_nat.v index f384e1488..f9c25739b 100644 --- a/theories/Arith/Bool_nat.v +++ b/theories/Arith/Bool_nat.v @@ -10,7 +10,7 @@ Require Export Compare_dec. Require Export Peano_dec. Require Import Sumbool. -Open Local Scope nat_scope. +Local Open Scope nat_scope. Implicit Types m n x y : nat. diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v index d0075d741..dc4da448e 100644 --- a/theories/Arith/Compare.v +++ b/theories/Arith/Compare.v @@ -8,7 +8,7 @@ (** Equality is decidable on [nat] *) -Open Local Scope nat_scope. +Local Open Scope nat_scope. Implicit Types m n p q : nat. diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index cc2d8efb5..1cb91f9a5 100644 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -11,7 +11,7 @@ Require Import Lt. Require Import Gt. Require Import Decidable. -Open Local Scope nat_scope. +Local Open Scope nat_scope. Implicit Types m n x y : nat. diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v index 94986278c..1dc69f612 100644 --- a/theories/Arith/EqNat.v +++ b/theories/Arith/EqNat.v @@ -8,7 +8,7 @@ (** Equality on natural numbers *) -Open Local Scope nat_scope. +Local Open Scope nat_scope. Implicit Types m n x y : nat. diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v index cd4dae98e..9a84a7f2e 100644 --- a/theories/Arith/Even.v +++ b/theories/Arith/Even.v @@ -10,7 +10,7 @@ and we prove the decidability and the exclusion of those predicates. The main results about parity are proved in the module Div2. *) -Open Local Scope nat_scope. +Local Open Scope nat_scope. Implicit Types m n : nat. diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v index e20626029..82643cdcd 100644 --- a/theories/Arith/Factorial.v +++ b/theories/Arith/Factorial.v @@ -9,7 +9,7 @@ Require Import Plus. Require Import Mult. Require Import Lt. -Open Local Scope nat_scope. +Local Open Scope nat_scope. (** Factorial *) diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v index 32f453e59..f9bf0f2fd 100644 --- a/theories/Arith/Gt.v +++ b/theories/Arith/Gt.v @@ -15,7 +15,7 @@ Definition gt (n m:nat) := m < n. Require Import Le. Require Import Lt. Require Import Plus. -Open Local Scope nat_scope. +Local Open Scope nat_scope. Implicit Types m n p : nat. diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v index f0ebf162b..717705a1c 100644 --- a/theories/Arith/Le.v +++ b/theories/Arith/Le.v @@ -16,7 +16,7 @@ where "n <= m" := (le n m) : nat_scope. >> *) -Open Local Scope nat_scope. +Local Open Scope nat_scope. Implicit Types m n p : nat. diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v index e07bba8d9..1f7e6e018 100644 --- a/theories/Arith/Lt.v +++ b/theories/Arith/Lt.v @@ -14,7 +14,7 @@ Infix "<" := lt : nat_scope. *) Require Import Le. -Open Local Scope nat_scope. +Local Open Scope nat_scope. Implicit Types m n p : nat. diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index bcfbe0efe..18e0e6af2 100644 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -10,7 +10,7 @@ Require Import NPeano. -Open Local Scope nat_scope. +Local Open Scope nat_scope. Implicit Types m n p : nat. Notation min := Peano.min (only parsing). diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v index ed215f540..7ec37a65e 100644 --- a/theories/Arith/Minus.v +++ b/theories/Arith/Minus.v @@ -21,7 +21,7 @@ where "n - m" := (minus n m) : nat_scope. Require Import Lt. Require Import Le. -Open Local Scope nat_scope. +Local Open Scope nat_scope. Implicit Types m n p : nat. diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index 479138a98..64b0d4dd3 100644 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -11,7 +11,7 @@ Require Export Minus. Require Export Lt. Require Export Le. -Open Local Scope nat_scope. +Local Open Scope nat_scope. Implicit Types m n p : nat. diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index 6eb667c11..e68ba9590 100644 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -9,7 +9,7 @@ Require Import Decidable. Require Eqdep_dec. Require Import Le Lt. -Open Local Scope nat_scope. +Local Open Scope nat_scope. Implicit Types m n x y : nat. diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v index 02975d8f1..c036d06e1 100644 --- a/theories/Arith/Plus.v +++ b/theories/Arith/Plus.v @@ -20,7 +20,7 @@ where "n + m" := (plus n m) : nat_scope. Require Import Le. Require Import Lt. -Open Local Scope nat_scope. +Local Open Scope nat_scope. Implicit Types m n p q : nat. diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index b4468dd1b..e264ccb5d 100644 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -10,7 +10,7 @@ Require Import Lt. -Open Local Scope nat_scope. +Local Open Scope nat_scope. Implicit Types m n p : nat. diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 92a584256..79a719a1f 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -754,7 +754,7 @@ Notation "a &&& b" := (if a then b else false) Notation "a ||| b" := (if a then true else b) (at level 50, left associativity) : lazy_bool_scope. -Open Local Scope lazy_bool_scope. +Local Open Scope lazy_bool_scope. Lemma andb_lazy_alt : forall a b : bool, a && b = a &&& b. Proof. diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index 0c2181638..2f904c81b 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -13,7 +13,7 @@ Require Vector. Export Vector.VectorNotations. Require Import Minus. -Open Local Scope nat_scope. +Local Open Scope nat_scope. (** We build bit vectors in the spirit of List.v. diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v index bac4c0d69..5689bf50d 100644 --- a/theories/Bool/Zerob.v +++ b/theories/Bool/Zerob.v @@ -9,7 +9,7 @@ Require Import Arith. Require Import Bool. -Open Local Scope nat_scope. +Local Open Scope nat_scope. Definition zerob (n:nat) : bool := match n with diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 87f86e0d3..29718276a 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -49,7 +49,7 @@ Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } := | right H => @left _ _ H end. -Open Local Scope program_scope. +Local Open Scope program_scope. (** Invert the branches. *) diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index 6d550dc93..6b2e62c92 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -26,7 +26,7 @@ Unset Strict Implicit. Generalizable Variables A R eqA B S eqB. Local Obligation Tactic := simpl_relation. -Open Local Scope signature_scope. +Local Open Scope signature_scope. Definition equiv `{Equivalence A R} : relation A := R. @@ -37,7 +37,7 @@ Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scop Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope. -Open Local Scope equiv_scope. +Local Open Scope equiv_scope. (** Overloading for [PER]. *) diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 8e491b1b8..0df835ab8 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -73,7 +73,7 @@ End ProperNotations. Export ProperNotations. -Open Local Scope signature_scope. +Local Open Scope signature_scope. (** [solve_proper] try to solve the goal [Proper (?==> ... ==>?) f] by repeated introductions and setoid rewrites. It should work diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 3717e1cb4..4c2c2dd0c 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -286,7 +286,7 @@ Definition predicate_implication {l : Tlist} := Infix "<∙>" := predicate_equivalence (at level 95, no associativity) : predicate_scope. Infix "-∙>" := predicate_implication (at level 70, right associativity) : predicate_scope. -Open Local Scope predicate_scope. +Local Open Scope predicate_scope. (** The pointwise liftings of conjunction and disjunctions. Note that these are [binary_operation]s, building new relations out of old ones. *) diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index a090d2007..693b724bc 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -50,7 +50,7 @@ Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } := Require Import Coq.Program.Program. -Open Local Scope program_scope. +Local Open Scope program_scope. (** Invert the branches. *) diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 31a4f5f25..5eab6370b 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -146,7 +146,7 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) Require Import Coq.Program.Tactics. -Open Local Scope signature_scope. +Local Open Scope signature_scope. Ltac red_subst_eq_morphism concl := match concl with diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index c761e2a7b..bed5ce742 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -32,9 +32,9 @@ Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. preservation *) Module Raw (Import I:Int)(X: OrderedType). -Open Local Scope pair_scope. -Open Local Scope lazy_bool_scope. -Open Local Scope Int_scope. +Local Open Scope pair_scope. +Local Open Scope lazy_bool_scope. +Local Open Scope Int_scope. Definition key := X.t. Hint Transparent key. diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index 774bcd9b3..e1c603514 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -34,8 +34,8 @@ Module AvlProofs (Import I:Int)(X: OrderedType). Module Import Raw := Raw I X. Module Import II:=MoreInt(I). Import Raw.Proofs. -Open Local Scope pair_scope. -Open Local Scope Int_scope. +Local Open Scope pair_scope. +Local Open Scope Int_scope. Ltac omega_max := i2z_refl; romega with Z. diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index 6d0315b82..d562245d8 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -11,7 +11,7 @@ Require Import Bool ZArith OrderedType OrderedTypeEx FMapInterface. Set Implicit Arguments. -Open Local Scope positive_scope. +Local Open Scope positive_scope. Local Unset Elimination Schemes. Local Unset Case Analysis Schemes. diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v index d35ed1389..653f7a70f 100644 --- a/theories/Logic/ClassicalDescription.v +++ b/theories/Logic/ClassicalDescription.v @@ -20,7 +20,7 @@ Require Export Classical. (* Axiomatize classical reasoning *) Require Export Description. (* Axiomatize constructive form of Church's iota *) Require Import ChoiceFacts. -Notation Local inhabited A := A (only parsing). +Local Notation inhabited A := A (only parsing). (** The idea for the following proof comes from [ChicliPottierSimpson02] *) diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index 7d5cec74d..2e1e99e8a 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -117,7 +117,7 @@ Qed. *) -Notation Local inhabited A := A (only parsing). +Local Notation inhabited A := A (only parsing). Lemma prop_ext_A_eq_A_imp_A : prop_extensionality -> forall A:Prop, inhabited A -> (A -> A) = A. diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v index 8dd51482c..6885f70a9 100644 --- a/theories/Logic/ConstructiveEpsilon.v +++ b/theories/Logic/ConstructiveEpsilon.v @@ -112,7 +112,7 @@ of our searching algorithm. *) Let R (x y : nat) : Prop := x = S y /\ ~ P y. -Notation Local acc x := (Acc R x). +Local Notation acc x := (Acc R x). Lemma P_implies_acc : forall x : nat, P x -> acc x. Proof. diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index d1327af3e..e8e8b94ce 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -265,7 +265,7 @@ End ProofIrrel_RelChoice_imp_EqEM. (** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *) -Notation Local inhabited A := A (only parsing). +Local Notation inhabited A := A (only parsing). Section ExtensionalEpsilon_imp_EM. @@ -279,7 +279,7 @@ Hypothesis epsilon_extensionality : forall (A:Type) (i:inhabited A) (P Q:A->Prop), (forall a, P a <-> Q a) -> epsilon A i P = epsilon A i Q. -Notation Local eps := (epsilon bool true) (only parsing). +Local Notation eps := (epsilon bool true) (only parsing). Theorem extensional_epsilon_imp_EM : forall P:Prop, P \/ ~ P. Proof. diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index 7cef5c5ad..f4ca4d680 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -29,7 +29,7 @@ Hint Unfold compose. Notation " g ∘ f " := (compose g f) (at level 40, left associativity) : program_scope. -Open Local Scope program_scope. +Local Open Scope program_scope. (** The non-dependent function space between [A] and [B]. *) diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index 4642021c4..24baf4598 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -10,7 +10,7 @@ Require Import Coq.Program.Utils. Require Import Coq.Program.Equality. -Open Local Scope program_scope. +Local Open Scope program_scope. (** The following tactics implement a poor-man's solution for proof-irrelevance: it tries to factorize every proof of the same proposition in a goal so that equality of such proofs becomes trivial. *) diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index ee0a7451b..8ef1eb4e6 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -12,7 +12,7 @@ Require Import Coq.Init.Wf. Require Import Coq.Program.Utils. Require Import ProofIrrelevance. -Open Local Scope program_scope. +Local Open Scope program_scope. Section Well_founded. Variable A : Type. diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v index cfc1fb141..54a6c3827 100644 --- a/theories/QArith/Qround.v +++ b/theories/QArith/Qround.v @@ -18,7 +18,7 @@ Hint Resolve Qopp_lt_compat : qarith. (************) -Coercion Local inject_Z : Z >-> Q. +Local Coercion inject_Z : Z >-> Q. Definition Qfloor (x:Q) := let (n,d) := x in Z.div n (Zpos d). Definition Qceiling (x:Q) := (-(Qfloor (-x)))%Z. diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index 18612a687..5e91accfe 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -13,7 +13,7 @@ Require Import SeqProp. Require Import PartSum. Require Import Max. -Open Local Scope R_scope. +Local Open Scope R_scope. (***************************************************) (* Various versions of the criterion of D'Alembert *) diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v index 87f1aaf72..227081cab 100644 --- a/theories/Reals/AltSeries.v +++ b/theories/Reals/AltSeries.v @@ -12,7 +12,7 @@ Require Import Rseries. Require Import SeqProp. Require Import PartSum. Require Import Max. -Open Local Scope R_scope. +Local Open Scope R_scope. (**********) (** * Formalization of alternated series *) diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v index 620561dcd..359b2855c 100644 --- a/theories/Reals/ArithProp.v +++ b/theories/Reals/ArithProp.v @@ -12,8 +12,8 @@ Require Import Even. Require Import Div2. Require Import ArithRing. -Open Local Scope Z_scope. -Open Local Scope R_scope. +Local Open Scope Z_scope. +Local Open Scope R_scope. Lemma minus_neq_O : forall n i:nat, (i < n)%nat -> (n - i)%nat <> 0%nat. Proof. diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v index 412f64428..a7bb4d9a6 100644 --- a/theories/Reals/Binomial.v +++ b/theories/Reals/Binomial.v @@ -9,7 +9,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import PartSum. -Open Local Scope R_scope. +Local Open Scope R_scope. Definition C (n p:nat) : R := INR (fact n) / (INR (fact p) * INR (fact (n - p))). diff --git a/theories/Reals/Cauchy_prod.v b/theories/Reals/Cauchy_prod.v index a9d5cde38..3019be9e8 100644 --- a/theories/Reals/Cauchy_prod.v +++ b/theories/Reals/Cauchy_prod.v @@ -10,7 +10,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Rseries. Require Import PartSum. -Open Local Scope R_scope. +Local Open Scope R_scope. (**********) Lemma sum_N_predN : diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v index ec1eeddf3..e966357ce 100644 --- a/theories/Reals/Cos_plus.v +++ b/theories/Reals/Cos_plus.v @@ -12,8 +12,8 @@ Require Import SeqSeries. Require Import Rtrigo_def. Require Import Cos_rel. Require Import Max. -Open Local Scope nat_scope. -Open Local Scope R_scope. +Local Open Scope nat_scope. +Local Open Scope R_scope. Definition Majxy (x y:R) (n:nat) : R := Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (4 * S n) / INR (fact n). diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v index 73f3c0c64..204e2009d 100644 --- a/theories/Reals/Cos_rel.v +++ b/theories/Reals/Cos_rel.v @@ -10,7 +10,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. Require Import Rtrigo_def. -Open Local Scope R_scope. +Local Open Scope R_scope. Definition A1 (x:R) (N:nat) : R := sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k)) * x ^ (2 * k)) N. diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v index 144de09e5..c21421b94 100644 --- a/theories/Reals/DiscrR.v +++ b/theories/Reals/DiscrR.v @@ -8,7 +8,7 @@ Require Import RIneq. Require Import Omega. -Open Local Scope R_scope. +Local Open Scope R_scope. Lemma Rlt_R0_R2 : 0 < 2. change 2 with (INR 2); apply lt_INR_0; apply lt_O_Sn. diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index 9a38888da..4b1b09406 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -15,8 +15,8 @@ Require Import PSeries_reg. Require Import Div2. Require Import Even. Require Import Max. -Open Local Scope nat_scope. -Open Local Scope R_scope. +Local Open Scope nat_scope. +Local Open Scope R_scope. Definition E1 (x:R) (N:nat) : R := sum_f_R0 (fun k:nat => / INR (fact k) * x ^ k) N. diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v index 29ebd46d8..b872e3fe3 100644 --- a/theories/Reals/MVT.v +++ b/theories/Reals/MVT.v @@ -10,7 +10,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis1. Require Import Rtopology. -Open Local Scope R_scope. +Local Open Scope R_scope. (* The Mean Value Theorem *) Theorem MVT : diff --git a/theories/Reals/Machin.v b/theories/Reals/Machin.v index 503e79a40..6b91719db 100644 --- a/theories/Reals/Machin.v +++ b/theories/Reals/Machin.v @@ -9,7 +9,7 @@ Require Import SeqProp. Require Import PartSum. Require Import Ratan. -Open Local Scope R_scope. +Local Open Scope R_scope. (* Proving a few formulas in the style of John Machin to compute Pi *) diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v index 8478a83e2..35192d0c4 100644 --- a/theories/Reals/NewtonInt.v +++ b/theories/Reals/NewtonInt.v @@ -11,7 +11,7 @@ Require Import Rfunctions. Require Import SeqSeries. Require Import Rtrigo1. Require Import Ranalysis. -Open Local Scope R_scope. +Local Open Scope R_scope. (*******************************************) (* Newton's Integral *) diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v index aa588e382..38de00030 100644 --- a/theories/Reals/PSeries_reg.v +++ b/theories/Reals/PSeries_reg.v @@ -12,7 +12,7 @@ Require Import SeqSeries. Require Import Ranalysis1. Require Import Max. Require Import Even. -Open Local Scope R_scope. +Local Open Scope R_scope. Definition Boule (x:R) (r:posreal) (y:R) : Prop := Rabs (y - x) < r. diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v index 3f90f15a0..3d9314b7d 100644 --- a/theories/Reals/PartSum.v +++ b/theories/Reals/PartSum.v @@ -11,7 +11,7 @@ Require Import Rfunctions. Require Import Rseries. Require Import Rcomplete. Require Import Max. -Open Local Scope R_scope. +Local Open Scope R_scope. Lemma tech1 : forall (An:nat -> R) (N:nat), diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v index dbd2e52ff..246d6dea9 100644 --- a/theories/Reals/RList.v +++ b/theories/Reals/RList.v @@ -8,7 +8,7 @@ Require Import Rbase. Require Import Rfunctions. -Open Local Scope R_scope. +Local Open Scope R_scope. Inductive Rlist : Type := | nil : Rlist diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v index c089b648d..9b64ea5f0 100644 --- a/theories/Reals/R_Ifp.v +++ b/theories/Reals/R_Ifp.v @@ -13,7 +13,7 @@ Require Import Rbase. Require Import Omega. -Open Local Scope R_scope. +Local Open Scope R_scope. (*********************************************************) (** * Fractional part *) diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v index f23b9f178..868b8617f 100644 --- a/theories/Reals/R_sqr.v +++ b/theories/Reals/R_sqr.v @@ -8,7 +8,7 @@ Require Import Rbase. Require Import Rbasic_fun. -Open Local Scope R_scope. +Local Open Scope R_scope. (****************************************************) (** Rsqr : some results *) diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v index 2c5ede239..47b9e6cf9 100644 --- a/theories/Reals/R_sqrt.v +++ b/theories/Reals/R_sqrt.v @@ -9,7 +9,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Rsqrt_def. -Open Local Scope R_scope. +Local Open Scope R_scope. (** * Continuous extension of Rsqrt on R *) Definition sqrt (x:R) : R := diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v index 3075bee8f..804bfe114 100644 --- a/theories/Reals/Ranalysis1.v +++ b/theories/Reals/Ranalysis1.v @@ -10,7 +10,7 @@ Require Import Rbase. Require Import Rfunctions. Require Export Rlimit. Require Export Rderiv. -Open Local Scope R_scope. +Local Open Scope R_scope. Implicit Type f : R -> R. (****************************************************) @@ -43,7 +43,7 @@ Notation "- x" := (opp_fct x) : Rfun_scope. Infix "*" := mult_fct : Rfun_scope. Infix "-" := minus_fct : Rfun_scope. Infix "/" := div_fct : Rfun_scope. -Notation Local "f1 'o' f2" := (comp f1 f2) +Local Notation "f1 'o' f2" := (comp f1 f2) (at level 20, right associativity) : Rfun_scope. Notation "/ x" := (inv_fct x) : Rfun_scope. diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v index 732a61017..218f2a38f 100644 --- a/theories/Reals/Ranalysis2.v +++ b/theories/Reals/Ranalysis2.v @@ -9,7 +9,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis1. -Open Local Scope R_scope. +Local Open Scope R_scope. (**********) Lemma formule : diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v index afd4a4ee8..aa9e6bb35 100644 --- a/theories/Reals/Ranalysis3.v +++ b/theories/Reals/Ranalysis3.v @@ -10,7 +10,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis1. Require Import Ranalysis2. -Open Local Scope R_scope. +Local Open Scope R_scope. (** Division *) Theorem derivable_pt_lim_div : diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v index 9b6e550aa..83bc28318 100644 --- a/theories/Reals/Ranalysis4.v +++ b/theories/Reals/Ranalysis4.v @@ -13,7 +13,7 @@ Require Import Rtrigo1. Require Import Ranalysis1. Require Import Ranalysis3. Require Import Exp_prop. -Open Local Scope R_scope. +Local Open Scope R_scope. (**********) Lemma derivable_pt_inv : diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v index f6abd2b01..c8a2e1a83 100644 --- a/theories/Reals/Ranalysis5.v +++ b/theories/Reals/Ranalysis5.v @@ -6,7 +6,7 @@ Require Import Fourier. Require Import RiemannInt. Require Import SeqProp. Require Import Max. -Open Local Scope R_scope. +Local Open Scope R_scope. (** * Preliminaries lemmas *) diff --git a/theories/Reals/Ranalysis_reg.v b/theories/Reals/Ranalysis_reg.v index 2026dd82e..2d4a3f15c 100644 --- a/theories/Reals/Ranalysis_reg.v +++ b/theories/Reals/Ranalysis_reg.v @@ -26,7 +26,7 @@ Require Export RList. Require Export Sqrt_reg. Require Export Ranalysis4. Require Export Rpower. -Open Local Scope R_scope. +Local Open Scope R_scope. Axiom AppVar : R. diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v index 01b429a08..597f95924 100644 --- a/theories/Reals/Ratan.v +++ b/theories/Reals/Ratan.v @@ -11,7 +11,7 @@ Require Import Ranalysis5. Require Import SeqSeries. Require Import PartSum. -Open Local Scope R_scope. +Local Open Scope R_scope. (** Tools *) diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index 259e1ac04..6a5b778f6 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -12,7 +12,7 @@ Require Export ZArith_base. Require Export Rdefinitions. -Open Local Scope R_scope. +Local Open Scope R_scope. (*********************************************************) (** * Field axioms *) diff --git a/theories/Reals/Rcomplete.v b/theories/Reals/Rcomplete.v index 77cb560cc..2841ac8e3 100644 --- a/theories/Reals/Rcomplete.v +++ b/theories/Reals/Rcomplete.v @@ -11,7 +11,7 @@ Require Import Rfunctions. Require Import Rseries. Require Import SeqProp. Require Import Max. -Open Local Scope R_scope. +Local Open Scope R_scope. (****************************************************) (* R is complete : *) diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index 83c6b82de..6f9f92176 100644 --- a/theories/Reals/Rdefinitions.v +++ b/theories/Reals/Rdefinitions.v @@ -21,7 +21,7 @@ Delimit Scope R_scope with R. (* Automatically open scope R_scope for arguments of type R *) Bind Scope R_scope with R. -Open Local Scope R_scope. +Local Open Scope R_scope. Parameter R0 : R. Parameter R1 : R. diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v index 8f9b99c28..0a6d728f5 100644 --- a/theories/Reals/Rderiv.v +++ b/theories/Reals/Rderiv.v @@ -16,7 +16,7 @@ Require Import Rfunctions. Require Import Rlimit. Require Import Fourier. Require Import Omega. -Open Local Scope R_scope. +Local Open Scope R_scope. (*********) Definition D_x (D:R -> Prop) (y x:R) : Prop := D x /\ y <> x. diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 4c4903cb2..940250273 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -535,7 +535,7 @@ Definition powerRZ (x:R) (n:Z) := | Zneg p => / x ^ Pos.to_nat p end. -Infix Local "^Z" := powerRZ (at level 30, right associativity) : R_scope. +Local Infix "^Z" := powerRZ (at level 30, right associativity) : R_scope. Lemma Zpower_NR0 : forall (x:Z) (n:nat), (0 <= x)%Z -> (0 <= Zpower_nat x n)%Z. diff --git a/theories/Reals/Rgeom.v b/theories/Reals/Rgeom.v index 5715f07f4..c00917b6b 100644 --- a/theories/Reals/Rgeom.v +++ b/theories/Reals/Rgeom.v @@ -11,7 +11,7 @@ Require Import Rfunctions. Require Import SeqSeries. Require Import Rtrigo1. Require Import R_sqrt. -Open Local Scope R_scope. +Local Open Scope R_scope. (** * Distance *) diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index 5b9c4bdd5..9e4a5e4b1 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -15,7 +15,7 @@ Require Import RiemannInt_SF. Require Import Classical_Prop. Require Import Classical_Pred_Type. Require Import Max. -Open Local Scope R_scope. +Local Open Scope R_scope. Set Implicit Arguments. diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index 18c24c184..abcb8d6ff 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -10,7 +10,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis_reg. Require Import Classical_Prop. -Open Local Scope R_scope. +Local Open Scope R_scope. Set Implicit Arguments. diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index 80b900af7..d2fee1fde 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -14,7 +14,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Fourier. -Open Local Scope R_scope. +Local Open Scope R_scope. (*******************************) (** * Calculus *) diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index b5bd2b734..019a2d96e 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -22,7 +22,7 @@ Require Import Rsqrt_def. Require Import R_sqrt. Require Import MVT. Require Import Ranalysis4. -Open Local Scope R_scope. +Local Open Scope R_scope. Lemma P_Rmin : forall (P:R -> Prop) (x y:R), P x -> P y -> P (Rmin x y). Proof. @@ -394,7 +394,7 @@ Qed. Definition Rpower (x y:R) := exp (y * ln x). -Infix Local "^R" := Rpower (at level 30, right associativity) : R_scope. +Local Infix "^R" := Rpower (at level 30, right associativity) : R_scope. (******************************************************************) (** * Properties of Rpower *) diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v index 12258d6b5..6bcf4bd4c 100644 --- a/theories/Reals/Rprod.v +++ b/theories/Reals/Rprod.v @@ -12,7 +12,7 @@ Require Import Rfunctions. Require Import Rseries. Require Import PartSum. Require Import Binomial. -Open Local Scope R_scope. +Local Open Scope R_scope. (** TT Ak; 0<=k<=N *) Fixpoint prod_f_R0 (f:nat -> R) (N:nat) : R := diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index 9d1ba7381..e67f118f6 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -9,7 +9,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Compare. -Open Local Scope R_scope. +Local Open Scope R_scope. Implicit Type r : R. diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v index 0027c2749..d26dcde21 100644 --- a/theories/Reals/Rsigma.v +++ b/theories/Reals/Rsigma.v @@ -10,7 +10,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Rseries. Require Import PartSum. -Open Local Scope R_scope. +Local Open Scope R_scope. Set Implicit Arguments. diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v index 223649ef5..ecde4f8bb 100644 --- a/theories/Reals/Rsqrt_def.v +++ b/theories/Reals/Rsqrt_def.v @@ -11,7 +11,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. Require Import Ranalysis1. -Open Local Scope R_scope. +Local Open Scope R_scope. Fixpoint Dichotomy_lb (x y:R) (P:R -> bool) (N:nat) {struct N} : R := match N with diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v index 814e336c2..77a4d5fbb 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -12,7 +12,7 @@ Require Import Ranalysis1. Require Import RList. Require Import Classical_Prop. Require Import Classical_Pred_Type. -Open Local Scope R_scope. +Local Open Scope R_scope. (** * General definitions and propositions *) diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index 4a405660c..3bb07fe0c 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -10,7 +10,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. Require Import Rtrigo_def. -Open Local Scope R_scope. +Local Open Scope R_scope. (***************************************************************) (** Using series definitions of cos and sin *) diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v index 90ba205f6..e77ea6e2d 100644 --- a/theories/Reals/Rtrigo_calc.v +++ b/theories/Reals/Rtrigo_calc.v @@ -11,7 +11,7 @@ Require Import Rfunctions. Require Import SeqSeries. Require Import Rtrigo1. Require Import R_sqrt. -Open Local Scope R_scope. +Local Open Scope R_scope. Lemma tan_PI : tan PI = 0. Proof. diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index 9b6edab68..2486e140f 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -7,7 +7,7 @@ (************************************************************************) Require Import Rbase Rfunctions SeqSeries Rtrigo_fun Max. -Open Local Scope R_scope. +Local Open Scope R_scope. (********************************) (** * Definition of exponential *) diff --git a/theories/Reals/Rtrigo_fun.v b/theories/Reals/Rtrigo_fun.v index 04deb0904..a946bc462 100644 --- a/theories/Reals/Rtrigo_fun.v +++ b/theories/Reals/Rtrigo_fun.v @@ -9,7 +9,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. -Open Local Scope R_scope. +Local Open Scope R_scope. (*****************************************************************) (** To define transcendental functions *) diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v index 0a05e6df4..a369d5ae2 100644 --- a/theories/Reals/Rtrigo_reg.v +++ b/theories/Reals/Rtrigo_reg.v @@ -12,8 +12,8 @@ Require Import SeqSeries. Require Import Rtrigo1. Require Import Ranalysis1. Require Import PSeries_reg. -Open Local Scope nat_scope. -Open Local Scope R_scope. +Local Open Scope nat_scope. +Local Open Scope R_scope. (**********) diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index 7b6eadc2f..fb1b81ac3 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -10,7 +10,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Rseries. Require Import Max. -Open Local Scope R_scope. +Local Open Scope R_scope. (*****************************************************************) (** Convergence properties of sequences *) diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v index 0d876be5d..3085d0200 100644 --- a/theories/Reals/SeqSeries.v +++ b/theories/Reals/SeqSeries.v @@ -19,7 +19,7 @@ Require Export Rsigma. Require Export Rprod. Require Export Cauchy_prod. Require Export Alembert. -Open Local Scope R_scope. +Local Open Scope R_scope. (**********) Lemma sum_maj1 : diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v index 4e704a274..c429567fe 100644 --- a/theories/Reals/Sqrt_reg.v +++ b/theories/Reals/Sqrt_reg.v @@ -10,7 +10,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis1. Require Import R_sqrt. -Open Local Scope R_scope. +Local Open Scope R_scope. (**********) Lemma sqrt_var_maj : diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 4f6fe3f86..c9e71e24a 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -137,7 +137,7 @@ Qed. which is typically not the case in coqide). *) -Open Local Scope char_scope. +Local Open Scope char_scope. Example Space := " ". Example DoubleQuote := """". diff --git a/theories/Strings/String.v b/theories/Strings/String.v index 958ecd4ff..289ffab31 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -24,7 +24,7 @@ Inductive string : Set := Delimit Scope string_scope with string. Bind Scope string_scope with string. -Open Local Scope string_scope. +Local Open Scope string_scope. (** Equality is decidable *) diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v index cac3cd4e5..8d535d509 100644 --- a/theories/ZArith/ZArith_dec.v +++ b/theories/ZArith/ZArith_dec.v @@ -11,7 +11,7 @@ Require Import Sumbool. Require Import BinInt. Require Import Zorder. Require Import Zcompare. -Open Local Scope Z_scope. +Local Open Scope Z_scope. (* begin hide *) (* Trivial, to deprecate? *) diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v index 3a86a821b..a38974339 100644 --- a/theories/ZArith/Zbool.v +++ b/theories/ZArith/Zbool.v @@ -13,7 +13,7 @@ Require Import Zcompare. Require Import ZArith_dec. Require Import Sumbool. -Open Local Scope Z_scope. +Local Open Scope Z_scope. (** * Boolean operations from decidability of order *) (** The decidability of equality and order relations over diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index dde0745eb..7ae2a67ca 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -10,7 +10,7 @@ Require Import ZArithRing. Require Import ZArith_base. Require Export Omega. Require Import Wf_nat. -Open Local Scope Z_scope. +Local Open Scope Z_scope. (**********************************************************************) diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v index bfd57d758..b871f9c98 100644 --- a/theories/ZArith/Zmisc.v +++ b/theories/ZArith/Zmisc.v @@ -11,7 +11,7 @@ Require Import BinInt. Require Import Zcompare. Require Import Zorder. Require Import Bool. -Open Local Scope Z_scope. +Local Open Scope Z_scope. (**********************************************************************) (** Iterators *) diff --git a/theories/ZArith/Zsqrt_compat.v b/theories/ZArith/Zsqrt_compat.v index 54f6f2e9a..0a5ad4ace 100644 --- a/theories/ZArith/Zsqrt_compat.v +++ b/theories/ZArith/Zsqrt_compat.v @@ -9,7 +9,7 @@ Require Import ZArithRing. Require Import Omega. Require Export ZArith_base. -Open Local Scope Z_scope. +Local Open Scope Z_scope. (** THIS FILE IS DEPRECATED diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v index efe5b6847..0a4418671 100644 --- a/theories/ZArith/Zwf.v +++ b/theories/ZArith/Zwf.v @@ -9,7 +9,7 @@ Require Import ZArith_base. Require Export Wf_nat. Require Import Omega. -Open Local Scope Z_scope. +Local Open Scope Z_scope. (** Well-founded relations on Z. *) |