Add an option to functions that need to be total

[andrew-johnson-4]

In Coq total functions must return a value matching their type signature. Exceptions and failures are not permitted. This could be added as a modifier to functions that can't fail.