diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-11-20 16:04:12 +0100 |
|---|---|---|
| committer |  Andres Erbsen <andreser@mit.edu> | 2017-11-20 10:04:12 -0500 |
| commit | caa187ddaa5e10f289c59b85844d7bc58817641b (patch) | |
| tree | 4c1a4f9bb0d920ab3b74be77ed875e302bbca471 /coqprime/Coqprime/Pmod.v | |
| parent | 3d2e80e1c91fd06197236405740e6b115b4addc4 (diff) | |
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).
Diffstat (limited to 'coqprime/Coqprime/Pmod.v')
| -rw-r--r-- | coqprime/Coqprime/Pmod.v | 6 |
1 files changed, 3 insertions, 3 deletions
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. |