Declared modules can improperly leak into modules and operators

[oskgo]

The current behaviour is that the modules and operators depending on the declared module refer to a nonexistent module when leaving the section.

Maybe we should handle the module case by making it parametric when leaving the section, but the operator case should just be prevented.

MRE:

theory Thy.
module type MT = {proc p():unit}. 
section.

declare module M <: MT.

op f: glob M.
module D = {
  proc p = M.p
}.

end section.
end Thy.

print Thy.

Ref #749