From b002bbdc743a551d6f1c110b8b4f3822958dbe50 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 6 Jul 2006 15:16:20 +0000
Subject: Typo

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9026 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Logic/ClassicalUniqueChoice.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v
index 7b9b09ef55..1fb69d3d3d 100644
--- a/theories/Logic/ClassicalUniqueChoice.v
+++ b/theories/Logic/ClassicalUniqueChoice.v
@@ -39,7 +39,7 @@ intros A B.
 apply (dependent_unique_choice A (fun _ => B)).
 Qed.
 
-(** The followig proof comes from [ChicliPottierSimpson02] *)
+(** The following proof comes from [ChicliPottierSimpson02] *)
 
 Require Import Setoid.
 
-- 
cgit v1.2.3