Dans l'état actuel du langage de tactique de Coq, de nombreux styles de développement sont possibles. Certains styles créent des preuves plus lisibles et plus robustes que d'autres. Une réflexion sur la meilleure manière de présenter une preuve est donc possible. Il y a cependant un compromis à faire entre le niveau de détail et l'encombrement visuel. Ainsi, le style défendu par SSReflect \cite{gonthier2010introduction} consiste à consacrer une unique ligne par étape du raisonnement mathématique. Les lignes sont donc longues, comprennent beaucoup de notations et ne sont pas forcément très lisibles mais les preuves obtenues tiennent en relativement peu de lignes et les utilisateurs expérimentés s'en accommodent.