Coq realizations should require to prove `goal`s (at least if they come from cloning)
Consider the following source code (say `f.mlw`)
```
module M1
use int.Int
constant c : int
axiom c_spec : c >= 17
constant d : int
axiom d_spec : d >= c
goal d_prop : d >= 10
end
module M2
use int.Int
constant c : int = 42
clone M1 with
constant c = c,
goal c_spec,
axiom .
goal d_moreprop : d >= 40
end
```
When trying to prove the goal in the IDE, I got exactly the tasks I expect: for the module `M1` I need to prove the goal `d_prop`, for `M2` I need to prove `c_spec` and `d_moreprop`.
If I ask to realize these modules in Coq, using commands
```
why3 realize -D coq-realize -L . -T f.M1 -o tmp
why3 realize -D coq-realize -L . -T f.M2 -o tmp
```
then for `M1.v` I have to define `c`, prove `c_spec`, define `d` and prove `d_spec`, but not to prove `d_prop`. That surprises me, although one could argue that when using the module M1, the goal `d_prop` would not be visible so not need to prove it.
for `M2.v` I need to define `d` and prove `d_spec` that's all. Not only I don't have to prove `d_moreprop`, similarly as before, but I don't need to prove `c_spec`. This seems to me a mistake, indeed a possible source of unsoundness of realizations.
Am I right? maybe @melquion some thoughts?
issue