aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-05-13 19:46:31 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-05-13 19:46:31 +0000
commit411a23ee7b6ceacf04a343e6523c16d430bd2af2 (patch)
treee88ab6d4fb392117a6b0b0a0d7323c27f9dce22e /theories
parentb99396f1ee52d285f4dca9cecc6e89b06105448f (diff)
typo
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8814 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
-rw-r--r--theories/ZArith/Znumtheory.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index b6ade8fd3..5c0ed2ec0 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -697,7 +697,7 @@ destruct a; unfold Zmod; simpl; intros; auto;
destruct (Zggcdn n r (Zpos p)) as (g,(rr,aa)); simpl; auto.
Qed.
-Lemma Zggcd_gcdn : forall a b, fst (Zggcd a b) = Zgcd a b.
+Lemma Zggcd_gcd : forall a b, fst (Zggcd a b) = Zgcd a b.
Proof.
intros; unfold Zggcd, Zgcd; apply Zggcdn_gcdn; auto.
Qed.