diff options
| author | letouzey | 2011-06-30 14:40:50 +0000 |
|---|---|---|
| committer | letouzey | 2011-06-30 14:40:50 +0000 |
| commit | 962c2260406c630e90bb001bd9238dea72eef0c1 (patch) | |
| tree | e32790d4a08c61c0128826a93b4b02203c7e18ce /theories/Numbers/Cyclic | |
| parent | e20e6b3b9e4148f62c94bfb467817feb2b6a4583 (diff) | |
Cleanup of Ndigits
- No need for compatibility notations for stuff introduced strictly
after branching of 8.3, for instance Nor, Nand, etc.
- Properties for N.lor, N.lxor, etc are now in BinNat.N, no need to
duplicate them in Ndigits, apart from the few compatibility results
about xor.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14249 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Cyclic')
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v index d92e818ffa..e6c5a0e04e 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v @@ -16,7 +16,7 @@ Require Import DoubleType. Local Open Scope Z_scope. -Local Infix "<<" := Pshiftl_nat (at level 30). +Local Infix "<<" := Pos.shiftl_nat (at level 30). Section DoubleBase. Variable w : Type. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v index bf92bbb987..062282f2ee 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v @@ -17,7 +17,7 @@ Require Import DoubleBase. Local Open Scope Z_scope. -Local Infix "<<" := Pshiftl_nat (at level 30). +Local Infix "<<" := Pos.shiftl_nat (at level 30). Section GENDIVN1. |