diff options
Diffstat (limited to 'theories/Numbers/Natural/Axioms/NStrongRec.v')
| -rw-r--r-- | theories/Numbers/Natural/Axioms/NStrongRec.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Numbers/Natural/Axioms/NStrongRec.v b/theories/Numbers/Natural/Axioms/NStrongRec.v index 5e8223108..a2e73f99a 100644 --- a/theories/Numbers/Natural/Axioms/NStrongRec.v +++ b/theories/Numbers/Natural/Axioms/NStrongRec.v @@ -1,7 +1,7 @@ -Require Import NAxioms. +Require Export NAxioms. -Module StrongRecProperties (Import NatModule : NatSignature). -Module Export DomainPropertiesModule := DomainProperties NatModule.DomainModule. +Module StrongRecProperties (NatModule : NatSignature). +Module Export NatPropertiesModule := NatProperties NatModule. Open Local Scope NScope. Section StrongRecursion. |