+ formal specification.
+
+%description -l pl
+Coq to narzêdzie pomagaj±ce w udowadnianiu, które:
+ - pozwala uporaæ siê z twierdzeniami dotycz±cymi rachunku
+ ró¿niczkowego,
+ - mechanicznie sprawdzaæ dowody tych twierdzeñ,
+ - pomagaæ w znalezieniu formalnych dowodów,
+ - wyci±gaæ program o dowiedzionej poprawno¶ci z konstruktywnego
+ dowodu jego formalnej specyfikacji.