diff options
Diffstat (limited to 'theories/Numbers/NatInt/NZOrder.v')
| -rw-r--r-- | theories/Numbers/NatInt/NZOrder.v | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index c6815ebf5..a95de8df7 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -12,7 +12,8 @@ Require Import NZAxioms NZBase Decidable OrderTac. -Module NZOrderProp (Import NZ : NZOrdSig)(Import NZBase : NZBaseProp NZ). +Module Type NZOrderPropSig + (Import NZ : NZOrdSig)(Import NZBase : NZBasePropSig NZ). Local Open Scope NumScope. Instance le_wd : Proper (eq==>eq==>iff) le. @@ -613,9 +614,11 @@ Qed. End WF. -End NZOrderProp. +End NZOrderPropSig. -Module NZOrderPropFunct (NZ : NZOrdSig) := NZBasePropFunct NZ <+ NZOrderProp NZ. +Module NZOrderPropFunct (Import NZ : NZOrdSig). + Include Type NZBasePropSig NZ <+ NZOrderPropSig NZ. +End NZOrderPropFunct. (** To Merge with GenericMinMax ... *) |