aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/NumPrelude.v
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-12-12 19:51:03 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-12-12 19:51:03 +0000
commit98a86e50e7dc06b77a34bf34a0476aebc07efbcd (patch)
tree177e015614f9c5cf3cdf798920322bc888a082d2 /theories/Numbers/NumPrelude.v
parenta19570bbbe7b42b491eae1cf33ff69a746584235 (diff)
Uniformity with the rest of the StdLib : _symm --> _sym
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11675 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/NumPrelude.v')
-rw-r--r--theories/Numbers/NumPrelude.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index 904145d50..14ea812f3 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -212,7 +212,7 @@ unfold reflexive, prod_rel.
destruct x; split; [apply (proj1 EA_equiv) | apply (proj1 EB_equiv)]; simpl.
Qed.
-Lemma prod_rel_symm : symmetric (A * B) prod_rel.
+Lemma prod_rel_sym : symmetric (A * B) prod_rel.
Proof.
unfold symmetric, prod_rel.
destruct x; destruct y;
@@ -229,7 +229,7 @@ Qed.
Theorem prod_rel_equiv : equiv (A * B) prod_rel.
Proof.
-unfold equiv; split; [exact prod_rel_refl | split; [exact prod_rel_trans | exact prod_rel_symm]].
+unfold equiv; split; [exact prod_rel_refl | split; [exact prod_rel_trans | exact prod_rel_sym]].
Qed.
End RelationOnProduct.