diff --git a/math/why3-gpl/Makefile b/math/why3-gpl/Makefile
index fed0023d6833..0963b89dff79 100644
--- a/math/why3-gpl/Makefile
+++ b/math/why3-gpl/Makefile
@@ -10,7 +10,7 @@ PKGNAMESUFFIX=	-gpl
 DISTNAME=	${PORTNAME}${PKGNAMESUFFIX}-${PORTVERSION}-src
 
 MAINTAINER=	marino@FreeBSD.org
-COMMENT=	Deductive program verification platform with SPARK support
+COMMENT=	Component of SPARK 2014
 
 LICENSE=	LGPL21 GPLv3
 LICENSE_COMB=	multi
diff --git a/math/why3-gpl/pkg-descr b/math/why3-gpl/pkg-descr
index 4ab076ae7288..c6a8b3de3be8 100644
--- a/math/why3-gpl/pkg-descr
+++ b/math/why3-gpl/pkg-descr
@@ -1,24 +1,5 @@
-Why3 is a platform for deductive program verification. It provides a rich
-language for specification and programming, called WhyML, and relies on
-external theorem provers, both automated and interactive, to discharge
-verification conditions. Why3 comes with a standard library of logical
-theories (integer and real arithmetic, Boolean operations, sets and maps,
-etc.) and basic programming data structures (arrays, queues, hash tables,
-etc.). A user can write WhyML programs directly and get correct-by-
-construction OCaml programs through an automated extraction mechanism.
-WhyML is also used as an intermediate language for the verification of C,
-Java, or Ada programs.
-
-Why3 is a complete reimplementation of the former Why platform. Among the
-new features are: numerous extensions to the input language, a new
-architecture for calling external provers, and a well-designed API,
-allowing to use Why3 as a software library. An important emphasis is put
-on modularity and genericity, giving the end user a possibility to easily
-reuse Why3 formalizations or to add support for a new external prover if
-wanted.
-
-This GPL version version of Why3 has been released by Adacore with an
-additional binary for SPARK 2014 support and some patches which have not
-yet been pushed upstream.
+This is a component of SPARK 2014.  Those looking for the deductive
+program verification platform known as why3 should refer to math/why3
+instead.
 
 WWW: https://forge.open-do.org/projects/spark2014