diff options
Diffstat (limited to 'theories/Numbers/Natural/Axioms/NStrongRec.v')
| -rw-r--r-- | theories/Numbers/Natural/Axioms/NStrongRec.v | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/theories/Numbers/Natural/Axioms/NStrongRec.v b/theories/Numbers/Natural/Axioms/NStrongRec.v index 5c9a65781..c35a6693b 100644 --- a/theories/Numbers/Natural/Axioms/NStrongRec.v +++ b/theories/Numbers/Natural/Axioms/NStrongRec.v @@ -1,7 +1,7 @@ Require Export NAxioms. -Module StrongRecProperties (Import NatModule : NatSignature). -Module Export NatPropertiesModule := NatProperties NatModule. +Module StrongRecProperties (Import NBaseMod : NBaseSig). +Module Export NBasePropMod := NBasePropFunct NBaseMod. Open Local Scope NatScope. Section StrongRecursion. @@ -66,3 +66,10 @@ End StrongRecursion. Implicit Arguments strong_rec [A]. End StrongRecProperties. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) |