Moving options to its own file and fixing a difference between reference manual and implementation.

In Definitions we demand types, while coq is sometimes lax about that.
Implementing some of the record definitions.
Fixing formatting for records.