diff options
Diffstat (limited to 'theories/Numbers/NatInt/NZAxioms.v')
| -rw-r--r-- | theories/Numbers/NatInt/NZAxioms.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index 8d56772ac..4dedcfe32 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -18,7 +18,7 @@ Require Export Equalities Orders NumPrelude GenericMinMax. *) Module Type ZeroSuccPred (Import T:Typ). - Parameter Inline zero : t. + Parameter Inline(20) zero : t. Parameters Inline succ pred : t -> t. End ZeroSuccPred. @@ -47,7 +47,7 @@ End IsNZDomain. *) Module Type OneTwo (Import T:Typ). - Parameter Inline one two : t. + Parameter Inline(20) one two : t. End OneTwo. Module Type OneTwoNotation (T:Typ)(Import NZ:OneTwo T). |