diff options
Diffstat (limited to 'theories/Numbers/Natural/Axioms/NOtherInd.v')
| -rw-r--r-- | theories/Numbers/Natural/Axioms/NOtherInd.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Numbers/Natural/Axioms/NOtherInd.v b/theories/Numbers/Natural/Axioms/NOtherInd.v index e37669bad..6f51330f3 100644 --- a/theories/Numbers/Natural/Axioms/NOtherInd.v +++ b/theories/Numbers/Natural/Axioms/NOtherInd.v @@ -1,5 +1,6 @@ Require Export NDomain. Declare Module Export DomainModule : DomainSignature. +Open Local Scope NScope. Parameter O : N. Parameter S : N -> N. |