aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Natural
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-10-10 18:54:56 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-10-10 21:23:01 +0200
commitd0cd27e209be08ee51a2d609157367f053438a10 (patch)
tree29c4f71268ab5cab9e6615732c66107ac1c84a71 /theories/Numbers/Natural
parent8a9de08c0e6a5130103cedf05cbcebcf5f621d1e (diff)
Give the same argument name for the record binder of type class
projections and regular records. Easily fixable backwards incompatibility.
Diffstat (limited to 'theories/Numbers/Natural')
-rw-r--r--theories/Numbers/Natural/BigN/Nbasic.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v
index e8a9940bd..338b5c7f9 100644
--- a/theories/Numbers/Natural/BigN/Nbasic.v
+++ b/theories/Numbers/Natural/BigN/Nbasic.v
@@ -20,8 +20,8 @@ Arguments mk_zn2z_ops [t] ops.
Arguments mk_zn2z_ops_karatsuba [t] ops.
Arguments mk_zn2z_specs [t ops] specs.
Arguments mk_zn2z_specs_karatsuba [t ops] specs.
-Arguments ZnZ.digits [t] Ops.
-Arguments ZnZ.zdigits [t] Ops.
+Arguments ZnZ.digits [t] Ops : rename.
+Arguments ZnZ.zdigits [t] Ops : rename.
Lemma Pshiftl_nat_Zpower : forall n p,
Zpos (Pos.shiftl_nat p n) = Zpos p * 2 ^ Z.of_nat n.