** Breaking change:

- to be consistent with oracle calls restrictions,
  negative memory restrictions are now set using a minus symbol
  (e.g. `(M <: T {-H})` instead of `(M <: T {H})`).

- use `pragma +old_mem_restr` to retrieve old behaviour on memory restrictions

** Additions:
- added a new hoare logic for cost, using predicates of
  the form `choare [H.f: pre ==> post] time [c]`, meaning:

  from any initial memory satisfying `pre`, the final memory obtained
  after the execution of `H.f` satisfies `post`, in time at most `c`

- in choare predicates, the cost `c` is a cost-vector, comprising:

  + a concrete cost of type `xint`, where `xint` is a algebraic data-type
    with two constructors, `N of int` (for bounded running times) and `Inf`
    (for potentially unbounded running times).

  + a list of abstract procedures together with an integer indicated the
    number of times they can be called (e.g. `ROM.o : 42`).

- complexity restrictions can be attached to module types procedures,
  restricting their instantiations.

- added a new predicate, `cost`, to establish the cost of evaluating an
  expression (while `choare` upper-bound the cost of a statement).

- (small) examples showing how to use the cost hoare logic can be found
  in the sub-directory `examples/cost/`

- more advanced examples, using a new UC framework in EasyCrypt, can
  be found in

  `examples/UC/composition_cost.ec`

  `examples/UC/dh_enc_cost.ec`