diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-02 21:19:10 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-02 21:19:10 +0000 |
| commit | ebcb4276f95764504c6b86a44e8ba2e2d91fc39c (patch) | |
| tree | fde0773b881fb62169c3b4eb2c88e66b7bd20763 /theories/Logic/ChoiceFacts.v | |
| parent | 7203757a679e32d52de2e7eb33ffaa1c59acb187 (diff) | |
Typo
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4774 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Logic/ChoiceFacts.v')
| -rw-r--r-- | theories/Logic/ChoiceFacts.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index d9d8b7670..699051ec1 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)). |