diff options
Diffstat (limited to 'theories/NArith/Ndigits.v')
| -rw-r--r-- | theories/NArith/Ndigits.v | 34 |
1 files changed, 18 insertions, 16 deletions
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index a1e51c9d..3ccaa721 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import Bool Morphisms Setoid Bvector BinPos BinNat PeanoNat Pnat Nnat. @@ -14,17 +16,17 @@ Local Open Scope N_scope. (** Compatibility names for some bitwise operations *) -Notation Pxor := Pos.lxor (compat "8.3"). -Notation Nxor := N.lxor (compat "8.3"). -Notation Pbit := Pos.testbit_nat (compat "8.3"). -Notation Nbit := N.testbit_nat (compat "8.3"). +Notation Pxor := Pos.lxor (only parsing). +Notation Nxor := N.lxor (only parsing). +Notation Pbit := Pos.testbit_nat (only parsing). +Notation Nbit := N.testbit_nat (only parsing). -Notation Nxor_eq := N.lxor_eq (compat "8.3"). -Notation Nxor_comm := N.lxor_comm (compat "8.3"). -Notation Nxor_assoc := N.lxor_assoc (compat "8.3"). -Notation Nxor_neutral_left := N.lxor_0_l (compat "8.3"). -Notation Nxor_neutral_right := N.lxor_0_r (compat "8.3"). -Notation Nxor_nilpotent := N.lxor_nilpotent (compat "8.3"). +Notation Nxor_eq := N.lxor_eq (only parsing). +Notation Nxor_comm := N.lxor_comm (only parsing). +Notation Nxor_assoc := N.lxor_assoc (only parsing). +Notation Nxor_neutral_left := N.lxor_0_l (only parsing). +Notation Nxor_neutral_right := N.lxor_0_r (only parsing). +Notation Nxor_nilpotent := N.lxor_nilpotent (only parsing). (** Equivalence of bit-testing functions, either with index in [N] or in [nat]. *) @@ -249,7 +251,7 @@ Local Close Scope N_scope. (** Checking whether a number is odd, i.e. if its lower bit is set. *) -Notation Nbit0 := N.odd (compat "8.3"). +Notation Nbit0 := N.odd (only parsing). Definition Nodd (n:N) := N.odd n = true. Definition Neven (n:N) := N.odd n = false. @@ -498,7 +500,7 @@ Qed. (** Number of digits in a number *) -Notation Nsize := N.size_nat (compat "8.3"). +Notation Nsize := N.size_nat (only parsing). (** conversions between N and bit vectors. *) |