diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-09 13:29:44 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-09 13:29:44 +0000 |
| commit | 23c9798e046e654a166c902a2bdd294c3a8a57b2 (patch) | |
| tree | 24d619728b6804aa01d434a37ec68ea2c7004f52 /theories/Init/Specif.v | |
| parent | e925e66c67eb0ff62b26fa4bc5694ea03a573ad9 (diff) | |
Bug 2767
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15291 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Init/Specif.v')
| -rw-r--r-- | theories/Init/Specif.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 637994b2b..5b7afc991 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -60,7 +60,7 @@ Add Printing Let sigT2. (** Projections of [sig] - An element [y] of a subset [{x:A & (P x)}] is the pair of an [a] + An element [y] of a subset [{x:A | (P x)}] is the pair of an [a] of type [A] and of a proof [h] that [a] satisfies [P]. Then [(proj1_sig y)] is the witness [a] and [(proj2_sig y)] is the proof of [(P a)] *) |