GitLab

In this way, we can always distinguish them from local theories and
modules. Both 'use Bool' and 'use why3.Bool' are accepted. No support
for use/clone of built-in modules is done yet, but so far we don't
needed (the only built-in module is why3.Prelude which is used by
default).

As of now, one cannot put a file "why3.why" at the root of loadpath,
since it will be inaccessible. Paths like why3/toto.why are still
admitted, but we will probably ban them too and reserve the whole
"why3.xxx.yyy" hierarchy for the built-in theories and modules.

syntax: clone type t 'a 'b = my_t ('b, 'a)

implicitly introduces a type alias for the RHS type
and accepts unknown type alises in a substitution,
provided every type in the ts_def is known.

+ rename Mlw_ty.ity_pure to ity_immutable

[bug 15011]

	Just a proposition for a more controllable why3replayer

can be used with the task in a session

Too bad, it does not seem to support quantifiers...

This reverts part of commit b45604c2.