#!/bin/sh
coqdoc -g --body-only --latex celebs.v
coqdoc -g celebs.v