Numbers: no need for advanced functions (e.g. sqrt) in NStrongRec, NDefOps, etc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13565 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 8 insertions, 5 deletions

diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index b360c016f3..78e38b3cf3 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -72,5 +72,8 @@ Axiom recursion_succ :
 
 End NAxiomsRec.
 
+Module Type NAxiomsRecSig := NAxiomsMiniSig <+ NAxiomsRec.
+Module Type NAxiomsRecSig' := NAxiomsMiniSig' <+ NAxiomsRec.
+
 Module Type NAxiomsFullSig := NAxiomsSig <+ NAxiomsRec.
 Module Type NAxiomsFullSig' := NAxiomsSig' <+ NAxiomsRec.
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index 8d11b5ce33..9af668487f 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -15,7 +15,7 @@ Require Export NStrongRec.
 (** In this module, we derive generic implementations of usual operators
    just via the use of a [recursion] function. *)
 
-Module NdefOpsProp (Import N : NAxiomsFullSig').
+Module NdefOpsProp (Import N : NAxiomsRecSig').
 Include NStrongRecProp N.
 
 (** Nullity Test *)
diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v
index 3a48b79972..1fe6ed9bf5 100644
--- a/theories/Numbers/Natural/Abstract/NIso.v
+++ b/theories/Numbers/Natural/Abstract/NIso.v
@@ -10,7 +10,7 @@
 
 Require Import NBase.
 
-Module Homomorphism (N1 N2 : NAxiomsFullSig).
+Module Homomorphism (N1 N2 : NAxiomsRecSig).
 
 Local Notation "n == m" := (N2.eq n m) (at level 70, no associativity).
 
@@ -51,7 +51,7 @@ Qed.
 
 End Homomorphism.
 
-Module Inverse (N1 N2 : NAxiomsFullSig).
+Module Inverse (N1 N2 : NAxiomsRecSig).
 
 Module Import NBasePropMod1 := NBaseProp N1.
 (* This makes the tactic induct available. Since it is taken from
@@ -74,7 +74,7 @@ Qed.
 
 End Inverse.
 
-Module Isomorphism (N1 N2 : NAxiomsFullSig).
+Module Isomorphism (N1 N2 : NAxiomsRecSig).
 
 Module Hom12 := Homomorphism N1 N2.
 Module Hom21 := Homomorphism N2 N1.
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index 26cf2d64a6..a52a52e766 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -13,7 +13,7 @@ and proves its properties *)
 
 Require Export NSub.
 
-Module NStrongRecProp (Import N : NAxiomsFullSig').
+Module NStrongRecProp (Import N : NAxiomsRecSig').
 Include NSubProp N.
 
 Section StrongRecursion.