minor changes
attempt at documenting coq's mysterious status