Anomalies: Instantiating clone with axiom, and closing section after (non-local) cloning subtheory of local clone.

[MM45]

Consider the following example, which describes two issues at once:
First, trying to (incorrectly?) instantiate an axiom with another one while cloning gives rise to an InvalidGoalShape anomaly (instead of giving a regular error message).
Second, cloning an abstract subtheory of a local clone prevents closing the section, giving an assertion failed anomaly.

require import AllCore PROM FinType.

type u.
clone FinType as FTu with type t <= u.

section.
local clone FullRO as FROu with type in_t <- u. 

(* anomaly: EcLib.EcCoreGoal.InvalidGoalShape
local clone FROu.FinEager as FEu with 
  axiom FinFrom.enum_spec <- FTu.enum_spec. 
*)
 
clone FROu.FinEager as FEu with theory FinFrom <- FTu.

(* anomaly: File "src/ecSection.ml", line 926, characters 4-10: Assertion failed *)
end section.