aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/Zgcd_alt.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith/Zgcd_alt.v')
-rw-r--r--theories/ZArith/Zgcd_alt.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v
index bcb9e42ae..ebf3d0246 100644
--- a/theories/ZArith/Zgcd_alt.v
+++ b/theories/ZArith/Zgcd_alt.v
@@ -22,7 +22,6 @@ Author: Pierre Letouzey
Require Import ZArith_base.
Require Import ZArithRing.
Require Import Zdiv.
-Require Import Zgcd_def.
Require Import Znumtheory.
Open Scope Z_scope.