diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/eqtype.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index 6832ea7..12b0601 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -437,7 +437,7 @@ End Endo. Variable aT : Type. -(* The invariant of an function f wrt a projection k is the pred of points *) +(* The invariant of a function f wrt a projection k is the pred of points *) (* that have the same projection as their image. *) Definition invariant (rT : eqType) f (k : aT -> rT) := |