Fix obsolete vernacular syntax for locality.

It was emitting a deprecation warning and will soon be removed from Coq.

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.