add documentation comments

I turned comments in the Coq files into documentation comments (for the
coqdoc tool) and added further documentation comment. In particular, I
added comments that give the definition of the evaluator for the lambda
calculi before defunctionalisation.