Functors in sections

[vbgl]

Following program is rejected by EasyCrypt with that message:

* In [lemmas or axioms]:/ [frag -1.0B])

lemma eq:
  forall (M_T <: T),
    equiv[ M_T.f ~ Sim(M_T).g : ={glob M_T} ==> ={glob M_T, res}].

[critical] [: line 1 (0) to line 39 (27)] call cannot be used with a lemma referring to `M.f/Sim(M).g': the last statement is a call to `M.f/M_T'.g'

module type T = {
  proc f(): bool
}.

module type T' (O : T) = {
  proc g(): bool
}.

module Sim (O : T) = {
  proc g() = {
    var r;

    r <@ O.f();
    return r;
  }
}.

section Bad.
declare module M_T <: T.

module M_T' = Sim(M_T). (* This should fail: M_T' should be required to be marked as local *)

equiv eq: M_T.f ~ M_T'.g: ={glob M_T} ==> ={glob M_T, res}.
proof. by proc *; inline *; sim. qed.
end section Bad.

print eq.

module M = {
  var b : bool

  proc f() = {
    b <- !b;
    return b;
  }
}.

equiv eq': M.f ~ M_T'.g: ={glob M} ==> ={glob M, res}.
proof. proc *. call (eq M).

[strub]

The module alias is correct, but its expansion when the section is closed is buggy.

[strub]

Related to #635. Once this is merged, I'll be able to do the proper generalization of module aliases.