diff options
| -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]. *) |