Skip to content

InvalidGoalShape when trying to instantiate an axiom in clone. #746

@strub

Description

@strub

See example:

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. 
*)

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No fields configured for Bug.

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions