diff options
| author | Yves Bertot | 2016-12-20 15:32:48 +0100 |
|---|---|---|
| committer | Yves Bertot | 2016-12-20 15:32:48 +0100 |
| commit | e7369f8e0115c2d32643d2eacd201362f32c9a34 (patch) | |
| tree | 42c4fd30b93c3a663d315124a61a00412d646058 /mathcomp/ssreflect | |
| parent | 29f6948c82da7ef51562a49d069583ffe77aa0ad (diff) | |
correct a typo in the documentation
Diffstat (limited to 'mathcomp/ssreflect')
| -rw-r--r-- | mathcomp/ssreflect/ssrbool.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/ssrbool.v b/mathcomp/ssreflect/ssrbool.v index bb8606f..c5a881f 100644 --- a/mathcomp/ssreflect/ssrbool.v +++ b/mathcomp/ssreflect/ssrbool.v @@ -113,7 +113,7 @@ Require Import ssrfun. (* Alternatively one can use the syntax for explicit simplifying predicates *) (* and relations (in the following x is bound in E): *) (* [pred x | E] == simplifying (see ssrfun) predicate x => E. *) -(* [pred x : T | E] == predicate x => T, with a cast on the argument. *) +(* [pred x : T | E] == predicate x => E, with a cast on the argument. *) (* [pred : T | P] == constant predicate P on type T. *) (* [pred x | E1 & E2] == [pred x | E1 && E2]; an x : T cast is allowed. *) (* [pred x in A] == [pred x | x in A]. *) |