From caa187ddaa5e10f289c59b85844d7bc58817641b Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 20 Nov 2017 16:04:12 +0100 Subject: Remove obsolete syntax for locality. (#270) This is preparing the landing of https://github.com/coq/coq/pull/1049. For now, I'm duplicating this patch which was already done upstream in CoqPrime, but please consider removing this ad-hoc copy (see discussion on PR #269). --- coqprime/Coqprime/Pmod.v | 6 +++--- coqprime/Coqprime/ZCmisc.v | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) (limited to 'coqprime') diff --git a/coqprime/Coqprime/Pmod.v b/coqprime/Coqprime/Pmod.v index 3075b10f9..fdaf321a2 100644 --- a/coqprime/Coqprime/Pmod.v +++ b/coqprime/Coqprime/Pmod.v @@ -9,9 +9,9 @@ Require Export ZArith. Require Export ZCmisc. -Open Local Scope positive_scope. +Local Open Scope positive_scope. -Open Local Scope P_scope. +Local Open Scope P_scope. (* [div_eucl a b] return [(q,r)] such that a = q*b + r *) Fixpoint div_eucl (a b : positive) {struct a} : N * N := @@ -143,7 +143,7 @@ Fixpoint Pmod (a b : positive) {struct a} : N := end. Infix "mod" := Pmod (at level 40, no associativity) : P_scope. -Open Local Scope P_scope. +Local Open Scope P_scope. Lemma Pmod_div_eucl : forall a b, a mod b = snd (a/b). Proof with auto. diff --git a/coqprime/Coqprime/ZCmisc.v b/coqprime/Coqprime/ZCmisc.v index 67709a146..ee6881849 100644 --- a/coqprime/Coqprime/ZCmisc.v +++ b/coqprime/Coqprime/ZCmisc.v @@ -7,7 +7,7 @@ (*************************************************************) Require Export ZArith. -Open Local Scope Z_scope. +Local Open Scope Z_scope. Coercion Zpos : positive >-> Z. Coercion Z_of_N : N >-> Z. @@ -88,10 +88,10 @@ Lemma Ppred_Zminus : forall p, 1< Zpos p -> (p-1)%Z = Ppred p. Proof. destruct p;simpl;trivial. intros;elimtype False;omega. Qed. -Open Local Scope positive_scope. +Local Open Scope positive_scope. Delimit Scope P_scope with P. -Open Local Scope P_scope. +Local Open Scope P_scope. Definition is_lt (n m : positive) := match (n ?= m) with -- cgit v1.2.3