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

3 files changed, 7 insertions, 7 deletions

diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 866bc95b8..668a11123 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -250,7 +250,7 @@ pr
  Qed.
 
  Theorem digits_nmake : forall n ww (w_op: ZnZ.Ops ww),
-    ZnZ.digits (nmake_op _ w_op n) = Pshiftl_nat (ZnZ.digits w_op) n.
+    ZnZ.digits (nmake_op _ w_op n) = Pos.shiftl_nat (ZnZ.digits w_op) n.
  Proof.
  induction n. auto.
  intros ww ww_op. rewrite Pshiftl_nat_S, <- IHn; auto.
@@ -333,7 +333,7 @@ pr "
  (** * Digits *)
 
  Lemma digits_make_op_0 : forall n,
-  ZnZ.digits (make_op n) = Pshiftl_nat (ZnZ.digits (dom_op Size)) (S n).
+  ZnZ.digits (make_op n) = Pos.shiftl_nat (ZnZ.digits (dom_op Size)) (S n).
  Proof.
  induction n.
  auto.
@@ -343,7 +343,7 @@ pr "
  Qed.
 
  Lemma digits_make_op : forall n,
-  ZnZ.digits (make_op n) = Pshiftl_nat (ZnZ.digits w0_op) (SizePlus (S n)).
+  ZnZ.digits (make_op n) = Pos.shiftl_nat (ZnZ.digits w0_op) (SizePlus (S n)).
  Proof.
  intros. rewrite digits_make_op_0.
  replace (SizePlus (S n)) with (S n + Size) by (rewrite <- plus_comm; auto).
@@ -351,7 +351,7 @@ pr "
  Qed.
 
  Lemma digits_dom_op : forall n,
-  ZnZ.digits (dom_op n) = Pshiftl_nat (ZnZ.digits w0_op) n.
+  ZnZ.digits (dom_op n) = Pos.shiftl_nat (ZnZ.digits w0_op) n.
  Proof.
  do_size (destruct n; try reflexivity).
  exact (digits_make_op n).
diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v
index dec8f1fe4..aed96a831 100644
--- a/theories/Numbers/Natural/BigN/Nbasic.v
+++ b/theories/Numbers/Natural/BigN/Nbasic.v
@@ -372,7 +372,7 @@ Section CompareRec.
  apply Zlt_le_trans with (1:= H).
  unfold double_wB, DoubleBase.double_wB; simpl.
  rewrite Pshiftl_nat_S, base_xO.
- set (u := base (Pshiftl_nat wm_base n)).
+ set (u := base (Pos.shiftl_nat wm_base n)).
  assert (0 < u).
   unfold u, base; auto with zarith.
  replace (u^2) with (u * u); simpl; auto with zarith.
@@ -507,7 +507,7 @@ Declare Instance dom_op n : ZnZ.Ops (dom_t n).
 Declare Instance dom_spec n : ZnZ.Specs (dom_op n).
 
 Axiom digits_dom_op : forall n,
-  ZnZ.digits (dom_op n) = Pshiftl_nat (ZnZ.digits (dom_op 0)) n.
+  ZnZ.digits (dom_op n) = Pos.shiftl_nat (ZnZ.digits (dom_op 0)) n.
 
 (** The type [t] of arbitrary-large numbers, with abstract constructor [mk_t]
     and destructor [destr_t] and iterator [iter_t] *)
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index a1f4ea9a2..0b40d1e6b 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import ZArith OrdersFacts Nnat Ndigits NAxioms NDiv NSig.
+Require Import ZArith OrdersFacts Nnat NAxioms NSig.
 
 (** * The interface [NSig.NType] implies the interface [NAxiomsSig] *)