aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-06-30 14:40:50 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-06-30 14:40:50 +0000
commit962c2260406c630e90bb001bd9238dea72eef0c1 (patch)
treee32790d4a08c61c0128826a93b4b02203c7e18ce /theories
parente20e6b3b9e4148f62c94bfb467817feb2b6a4583 (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')
-rw-r--r--theories/NArith/Ndigits.v219
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v2
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v2
-rw-r--r--theories/Numbers/Natural/BigN/NMake_gen.ml8
-rw-r--r--theories/Numbers/Natural/BigN/Nbasic.v4
-rw-r--r--theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v2
6 files changed, 75 insertions, 162 deletions
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index e13d6ac51..b0c335957 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -13,145 +13,139 @@ Local Open Scope N_scope.
(** This file is mostly obsolete, see directly [BinNat] now. *)
-(** Operation over bits of a [N] number. *)
-
-Notation Por := Pos.lor (only parsing).
-Notation Nor := N.lor (only parsing).
-Notation Pand := Pos.land (only parsing).
-Notation Nand := N.land (only parsing).
-Notation Pdiff := Pos.ldiff (only parsing).
-Notation Ndiff := N.ldiff (only parsing).
+(** Compatibility names for some bitwise operations *)
+
Notation Pxor := Pos.lxor (only parsing).
Notation Nxor := N.lxor (only parsing).
-Notation Nshiftl_nat := N.shiftl_nat (only parsing).
-Notation Nshiftr_nat := N.shiftr_nat (only parsing).
-Notation Nshiftl := N.shiftl (only parsing).
-Notation Nshiftr := N.shiftr (only parsing).
Notation Pbit := Pos.testbit_nat (only parsing).
Notation Nbit := N.testbit_nat (only parsing).
-Notation Ptestbit := Pos.testbit (only parsing).
-Notation Ntestbit := N.testbit (only parsing).
-(** Equivalence of Pbit and Ptestbit *)
+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]. *)
Lemma Ptestbit_Pbit :
- forall p n, Ptestbit p (N_of_nat n) = Pbit p n.
+ forall p n, Pos.testbit p (N.of_nat n) = Pbit p n.
Proof.
induction p as [p IH|p IH| ]; intros [|n]; simpl; trivial;
rewrite <- IH; f_equal; rewrite (pred_Sn n) at 2; now rewrite N_of_pred.
Qed.
-Lemma Ntestbit_Nbit : forall a n, Ntestbit a (N_of_nat n) = Nbit a n.
+Lemma Ntestbit_Nbit : forall a n, N.testbit a (N.of_nat n) = Nbit a n.
Proof.
destruct a. trivial. apply Ptestbit_Pbit.
Qed.
Lemma Pbit_Ptestbit :
- forall p n, Pbit p (nat_of_N n) = Ptestbit p n.
+ forall p n, Pbit p (N.to_nat n) = Pos.testbit p n.
Proof.
- intros; now rewrite <- Ptestbit_Pbit, N_of_nat_of_N.
+ intros; now rewrite <- Ptestbit_Pbit, N2Nat.id.
Qed.
Lemma Nbit_Ntestbit :
- forall a n, Nbit a (nat_of_N n) = Ntestbit a n.
+ forall a n, Nbit a (N.to_nat n) = N.testbit a n.
Proof.
destruct a. trivial. apply Pbit_Ptestbit.
Qed.
-(** Equivalence of shifts, N and nat versions *)
+(** Equivalence of shifts, index in [N] or [nat] *)
Lemma Nshiftr_nat_S : forall a n,
- Nshiftr_nat a (S n) = Ndiv2 (Nshiftr_nat a n).
+ N.shiftr_nat a (S n) = N.div2 (N.shiftr_nat a n).
Proof.
reflexivity.
Qed.
Lemma Nshiftl_nat_S : forall a n,
- Nshiftl_nat a (S n) = Ndouble (Nshiftl_nat a n).
+ N.shiftl_nat a (S n) = N.double (N.shiftl_nat a n).
Proof.
reflexivity.
Qed.
Lemma Nshiftr_nat_equiv :
- forall a n, Nshiftr_nat a (nat_of_N n) = Nshiftr a n.
+ forall a n, N.shiftr_nat a (N.to_nat n) = N.shiftr a n.
Proof.
- intros a [|n]; simpl. unfold Nshiftr_nat.
+ intros a [|n]; simpl. unfold N.shiftr_nat.
trivial.
symmetry. apply iter_nat_of_P.
Qed.
Lemma Nshiftr_equiv_nat :
- forall a n, Nshiftr a (N_of_nat n) = Nshiftr_nat a n.
+ forall a n, N.shiftr a (N.of_nat n) = N.shiftr_nat a n.
Proof.
- intros. now rewrite <- Nshiftr_nat_equiv, nat_of_N_of_nat.
+ intros. now rewrite <- Nshiftr_nat_equiv, Nat2N.id.
Qed.
Lemma Nshiftl_nat_equiv :
- forall a n, Nshiftl_nat a (nat_of_N n) = Nshiftl a n.
+ forall a n, N.shiftl_nat a (N.to_nat n) = N.shiftl a n.
Proof.
- intros [|a] [|n]; simpl; unfold Nshiftl_nat; trivial.
- apply iter_nat_invariant; intros; now subst.
- rewrite <- iter_nat_of_P. symmetry. now apply iter_pos_swap_gen.
+ intros [|a] [|n]; simpl; unfold N.shiftl_nat; trivial.
+ apply nat_iter_invariant; intros; now subst.
+ rewrite <- Pos2Nat.inj_iter. symmetry. now apply Pos.iter_swap_gen.
Qed.
Lemma Nshiftl_equiv_nat :
- forall a n, Nshiftl a (N_of_nat n) = Nshiftl_nat a n.
+ forall a n, N.shiftl a (N.of_nat n) = N.shiftl_nat a n.
Proof.
- intros. now rewrite <- Nshiftl_nat_equiv, nat_of_N_of_nat.
+ intros. now rewrite <- Nshiftl_nat_equiv, Nat2N.id.
Qed.
(** Correctness proofs for shifts, nat version *)
Lemma Nshiftr_nat_spec : forall a n m,
- Nbit (Nshiftr_nat a n) m = Nbit a (m+n).
+ Nbit (N.shiftr_nat a n) m = Nbit a (m+n).
Proof.
induction n; intros m.
now rewrite <- plus_n_O.
simpl. rewrite <- plus_n_Sm, <- plus_Sn_m, <- IHn, Nshiftr_nat_S.
- destruct (Nshiftr_nat a n) as [|[p|p|]]; simpl; trivial.
+ destruct (N.shiftr_nat a n) as [|[p|p|]]; simpl; trivial.
Qed.
Lemma Nshiftl_nat_spec_high : forall a n m, (n<=m)%nat ->
- Nbit (Nshiftl_nat a n) m = Nbit a (m-n).
+ Nbit (N.shiftl_nat a n) m = Nbit a (m-n).
Proof.
induction n; intros m H.
now rewrite <- minus_n_O.
destruct m. inversion H. apply le_S_n in H.
simpl. rewrite <- IHn, Nshiftl_nat_S; trivial.
- destruct (Nshiftl_nat a n) as [|[p|p|]]; simpl; trivial.
+ destruct (N.shiftl_nat a n) as [|[p|p|]]; simpl; trivial.
Qed.
Lemma Nshiftl_nat_spec_low : forall a n m, (m<n)%nat ->
- Nbit (Nshiftl_nat a n) m = false.
+ Nbit (N.shiftl_nat a n) m = false.
Proof.
induction n; intros m H. inversion H.
rewrite Nshiftl_nat_S.
destruct m.
- destruct (Nshiftl_nat a n); trivial.
+ destruct (N.shiftl_nat a n); trivial.
specialize (IHn m (lt_S_n _ _ H)).
- destruct (Nshiftl_nat a n); trivial.
+ destruct (N.shiftl_nat a n); trivial.
Qed.
(** A left shift for positive numbers (used in BigN) *)
-Notation Pshiftl_nat := Pos.shiftl_nat (only parsing).
-
-Lemma Pshiftl_nat_0 : forall p, Pshiftl_nat p 0 = p.
+Lemma Pshiftl_nat_0 : forall p, Pos.shiftl_nat p 0 = p.
Proof. reflexivity. Qed.
Lemma Pshiftl_nat_S :
- forall p n, Pshiftl_nat p (S n) = xO (Pshiftl_nat p n).
+ forall p n, Pos.shiftl_nat p (S n) = xO (Pos.shiftl_nat p n).
Proof. reflexivity. Qed.
Lemma Pshiftl_nat_N :
- forall p n, Npos (Pshiftl_nat p n) = Nshiftl_nat (Npos p) n.
+ forall p n, Npos (Pos.shiftl_nat p n) = N.shiftl_nat (Npos p) n.
Proof.
- unfold Pshiftl_nat, Nshiftl_nat.
+ unfold Pos.shiftl_nat, N.shiftl_nat.
induction n; simpl; auto. now rewrite <- IHn.
Qed.
Lemma Pshiftl_nat_plus : forall n m p,
- Pshiftl_nat p (m + n) = Pshiftl_nat (Pshiftl_nat p n) m.
+ Pos.shiftl_nat p (m + n) = Pos.shiftl_nat (Pos.shiftl_nat p n) m.
Proof.
induction m; simpl; intros. reflexivity.
rewrite 2 Pshiftl_nat_S. now f_equal.
@@ -159,71 +153,54 @@ Qed.
(** Semantics of bitwise operations with respect to [Nbit] *)
-Lemma Pxor_semantics : forall p p' n,
- Nbit (Pxor p p') n = xorb (Pbit p n) (Pbit p' n).
+Lemma Pxor_semantics p p' n :
+ Nbit (Pos.lxor p p') n = xorb (Pbit p n) (Pbit p' n).
Proof.
- induction p as [p IHp|p IHp|]; intros [p'|p'|] [|n]; trivial; simpl;
- (specialize (IHp p'); destruct Pxor; trivial; apply (IHp n)) ||
- now destruct Pbit.
+ rewrite <- Ntestbit_Nbit, <- !Ptestbit_Pbit. apply N.pos_lxor_spec.
Qed.
-Lemma Nxor_semantics : forall a a' n,
- Nbit (Nxor a a') n = xorb (Nbit a n) (Nbit a' n).
+Lemma Nxor_semantics a a' n :
+ Nbit (N.lxor a a') n = xorb (Nbit a n) (Nbit a' n).
Proof.
- intros [|p] [|p'] n; simpl; trivial.
- now destruct Pbit.
- now destruct Pbit.
- apply Pxor_semantics.
+ rewrite <- !Ntestbit_Nbit. apply N.lxor_spec.
Qed.
-Lemma Por_semantics : forall p p' n,
- Pbit (Por p p') n = (Pbit p n) || (Pbit p' n).
+Lemma Por_semantics p p' n :
+ Pbit (Pos.lor p p') n = (Pbit p n) || (Pbit p' n).
Proof.
- induction p as [p IHp|p IHp|]; intros [p'|p'|] [|n]; trivial;
- apply (IHp p' n) || now rewrite orb_false_r.
+ rewrite <- !Ptestbit_Pbit. apply N.pos_lor_spec.
Qed.
-Lemma Nor_semantics : forall a a' n,
- Nbit (Nor a a') n = (Nbit a n) || (Nbit a' n).
+Lemma Nor_semantics a a' n :
+ Nbit (N.lor a a') n = (Nbit a n) || (Nbit a' n).
Proof.
- intros [|p] [|p'] n; simpl; trivial.
- now rewrite orb_false_r.
- apply Por_semantics.
+ rewrite <- !Ntestbit_Nbit. apply N.lor_spec.
Qed.
-Lemma Pand_semantics : forall p p' n,
- Nbit (Pand p p') n = (Pbit p n) && (Pbit p' n).
+Lemma Pand_semantics p p' n :
+ Nbit (Pos.land p p') n = (Pbit p n) && (Pbit p' n).
Proof.
- induction p as [p IHp|p IHp|]; intros [p'|p'|] [|n]; trivial; simpl;
- (specialize (IHp p'); destruct Pand; trivial; apply (IHp n)) ||
- now rewrite andb_false_r.
+ rewrite <- Ntestbit_Nbit, <- !Ptestbit_Pbit. apply N.pos_land_spec.
Qed.
-Lemma Nand_semantics : forall a a' n,
- Nbit (Nand a a') n = (Nbit a n) && (Nbit a' n).
+Lemma Nand_semantics a a' n :
+ Nbit (N.land a a') n = (Nbit a n) && (Nbit a' n).
Proof.
- intros [|p] [|p'] n; simpl; trivial.
- now rewrite andb_false_r.
- apply Pand_semantics.
+ rewrite <- !Ntestbit_Nbit. apply N.land_spec.
Qed.
-Lemma Pdiff_semantics : forall p p' n,
- Nbit (Pdiff p p') n = (Pbit p n) && negb (Pbit p' n).
+Lemma Pdiff_semantics p p' n :
+ Nbit (Pos.ldiff p p') n = (Pbit p n) && negb (Pbit p' n).
Proof.
- induction p as [p IHp|p IHp|]; intros [p'|p'|] [|n]; trivial; simpl;
- (specialize (IHp p'); destruct Pdiff; trivial; apply (IHp n)) ||
- now rewrite andb_true_r.
+ rewrite <- Ntestbit_Nbit, <- !Ptestbit_Pbit. apply N.pos_ldiff_spec.
Qed.
-Lemma Ndiff_semantics : forall a a' n,
- Nbit (Ndiff a a') n = (Nbit a n) && negb (Nbit a' n).
+Lemma Ndiff_semantics a a' n :
+ Nbit (N.ldiff a a') n = (Nbit a n) && negb (Nbit a' n).
Proof.
- intros [|p] [|p'] n; simpl; trivial.
- simpl. now rewrite andb_true_r.
- apply Pdiff_semantics.
+ rewrite <- !Ntestbit_Nbit. apply N.ldiff_spec.
Qed.
-
(** Equality over functional streams of bits *)
Definition eqf (f g:nat -> bool) := forall n:nat, f n = g n.
@@ -265,70 +242,6 @@ Proof.
split. apply Nbit_faithful. intros; now subst.
Qed.
-Hint Rewrite Nxor_semantics Nor_semantics
- Nand_semantics Ndiff_semantics : bitwise_semantics.
-
-Ltac bitwise_semantics :=
- apply Nbit_faithful; intro n; autorewrite with bitwise_semantics.
-
-(** Now, we can easily deduce properties of [Nxor] and others
- from properties of [xorb] and others. *)
-
-Definition Nxor_eq : forall a a', Nxor a a' = 0 -> a = a' := N.lxor_eq.
-Definition Nxor_nilpotent : forall a, Nxor a a = 0 := N.lxor_nilpotent.
-Definition Nxor_0_l : forall n, Nxor 0 n = n := N.lxor_0_l.
-Definition Nxor_0_r : forall n, Nxor n 0 = n := N.lxor_0_r.
-
-Notation Nxor_neutral_left := Nxor_0_l (only parsing).
-Notation Nxor_neutral_right := Nxor_0_r (only parsing).
-
-Definition Nxor_comm : forall a a', Nxor a a' = Nxor a' a := N.lxor_comm.
-
-Definition Nxor_assoc :
- forall a a' a'', Nxor (Nxor a a') a'' = Nxor a (Nxor a' a'')
- := N.lxor_assoc.
-
-Definition Nor_0_l : forall n, Nor 0 n = n := N.lor_0_l.
-Definition Nor_0_r : forall n, Nor n 0 = n := N.lor_0_r.
-Definition Nor_comm : forall a a', Nor a a' = Nor a' a := N.lor_comm.
-Definition Nor_assoc :
- forall a a' a'', Nor a (Nor a' a'') = Nor (Nor a a') a''
- := N.lor_assoc.
-Definition Nor_diag : forall a, Nor a a = a := N.lor_diag.
-
-Definition Nand_0_l : forall n, Nand 0 n = 0 := N.land_0_l.
-Definition Nand_0_r : forall n, Nand n 0 = 0 := N.land_0_r.
-Definition Nand_comm : forall a a', Nand a a' = Nand a' a := N.land_comm.
-Definition Nand_assoc :
- forall a a' a'', Nand a (Nand a' a'') = Nand (Nand a a') a''
- := N.land_assoc.
-Definition Nand_diag : forall a, Nand a a = a := N.land_diag.
-
-Definition Ndiff_0_l : forall n, Ndiff 0 n = 0 := N.ldiff_0_l.
-Definition Ndiff_0_r : forall n, Ndiff n 0 = n := N.ldiff_0_r.
-Definition Ndiff_diag : forall a, Ndiff a a = 0 := N.ldiff_diag.
-Definition Nor_and_distr_l : forall a b c,
- Nor (Nand a b) c = Nand (Nor a c) (Nor b c)
- := N.lor_land_distr_l.
-Definition Nor_and_distr_r : forall a b c,
- Nor a (Nand b c) = Nand (Nor a b) (Nor a c)
- := N.lor_land_distr_r.
-Definition Nand_or_distr_l : forall a b c,
- Nand (Nor a b) c = Nor (Nand a c) (Nand b c)
- := N.land_lor_distr_l.
-Definition Nand_or_distr_r : forall a b c,
- Nand a (Nor b c) = Nor (Nand a b) (Nand a c)
- := N.land_lor_distr_r.
-Definition Ndiff_diff_l : forall a b c,
- Ndiff (Ndiff a b) c = Ndiff a (Nor b c)
- := N.ldiff_ldiff_l.
-Definition Nor_diff_and : forall a b,
- Nor (Ndiff a b) (Nand a b) = a
- := N.lor_ldiff_and.
-Definition Nand_diff : forall a b,
- Nand (Ndiff a b) b = 0
- := N.land_ldiff.
-
Local Close Scope N_scope.
(** Checking whether a number is odd, i.e.
@@ -742,7 +655,7 @@ destruct a, b, (Bv2N n v1), (Bv2N n v2); simpl in *; rewrite H ; now simpl.
Qed.
Lemma Nand_BVand : forall n (bv bv' : Bvector n),
- Bv2N _ (BVand _ bv bv') = Nand (Bv2N _ bv) (Bv2N _ bv').
+ Bv2N _ (BVand _ bv bv') = N.land (Bv2N _ bv) (Bv2N _ bv').
Proof.
refine (@Vector.rect2 _ _ _ _ _); simpl; intros; auto.
rewrite H.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
index d92e818ff..e6c5a0e04 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 bf92bbb98..062282f2e 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.
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] *)