\documentclass[12pt]{article}
\usepackage[]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{fullpage}
\usepackage{coqdoc}
\def\name#1{{\sc #1}}
\title{Proved Program Of The Month: Celebrities in a party.}
\author{Matthieu Sozeau}
\def\coqdocmodule#1{}
\begin{document}

\maketitle

\input{celebs}

\end{document}
%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: