diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract/ZAdd.v')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZAdd.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v index aff298117..2c386a980 100644 --- a/theories/Numbers/Integer/Abstract/ZAdd.v +++ b/theories/Numbers/Integer/Abstract/ZAdd.v @@ -10,8 +10,8 @@ Require Export ZBase. -Module ZAddPropFunct (Import Z : ZAxiomsSig'). -Include ZBasePropFunct Z. +Module ZAddProp (Import Z : ZAxiomsMiniSig'). +Include ZBaseProp Z. (** Theorems that are either not valid on N or have different proofs on N and Z *) @@ -287,5 +287,5 @@ Qed. (** Of course, there are many other variants *) -End ZAddPropFunct. +End ZAddProp. |