diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract/ZAddOrder.v')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZAddOrder.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v index bdc4d21e9..eb27e6378 100644 --- a/theories/Numbers/Integer/Abstract/ZAddOrder.v +++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v @@ -10,8 +10,8 @@ Require Export ZLt. -Module ZAddOrderPropFunct (Import Z : ZAxiomsSig'). -Include ZOrderPropFunct Z. +Module ZAddOrderProp (Import Z : ZAxiomsMiniSig'). +Include ZOrderProp Z. (** Theorems that are either not valid on N or have different proofs on N and Z *) @@ -293,6 +293,6 @@ End PosNeg. Ltac zero_pos_neg n := induction_maker n ltac:(apply zero_pos_neg). -End ZAddOrderPropFunct. +End ZAddOrderProp. |