aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Integer/Abstract/ZAxioms.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/Integer/Abstract/ZAxioms.v')
-rw-r--r--theories/Numbers/Integer/Abstract/ZAxioms.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index ab863eb1f..bde3d9a92 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -10,7 +10,7 @@ Open Local Scope NatIntScope.
Notation Z := NZ (only parsing).
Notation E := NZE (only parsing).
-Parameter Inline Zopp : Z -> Z.
+Parameter Zopp : Z -> Z.
Add Morphism Zopp with signature E ==> E as Zopp_wd.