Section refactor

I've replaced the syntax, semantics and macros sections by functors. The 3 functors take a Module of signature:

Module Type ContractContext.
  Parameter get_contract_type : contract_constant -> M type.
  Parameter self_type : type.
End ContractContext.

In order to prove a contract, the programmer has to instantiate a Semantics module like so:

Module ContractContext <: syntax.ContractContext.
  Axiom get_contract_type : contract_constant -> error.M type.
  Definition self_type := Comparable_type parameter_ty.
End ContractContext.
Module Semantics := Semantics ContractContext. Import Semantics.

where parameter_ty is the type of the parameter of the contract proved. For convenience, the Semantics module also exports the contents of the Syntax and Macros functors.