From ebcb4276f95764504c6b86a44e8ba2e2d91fc39c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 2 Nov 2003 21:19:10 +0000
Subject: Typo

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

diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index d9d8b76706..699051ec15 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -112,7 +112,7 @@ Exists y. Split.
       NewDestruct HR''xy' as [H'Px HR'xy'].
       Rewrite proof_irrel with a1:=HPx a2:=H'Px.
       Exact HR'xy'.
-.Qed.
+Qed.
 
 Definition IndependenceOfPremises :=
  (A:Type)(P:A->Prop)(Q:Prop)(Q->(EXT x|(P x)))->(EXT x|Q->(P x)).
-- 
cgit v1.2.3