better error message for missing join?

[affeldt-aist]

A missing join gives rise to an error message such that

Error:
You must declare the current class indt «axioms_» before
indt «Blah.axioms_»

that suggests that the situation could be fixed by swapping declarations whereas the
explicit declaration of a new structure seems required.

If there is nothing to improve than this might be considered as a FAQ entry @gares .

This is the case for example for the following script:

From HB Require Import structures.

HB.mixin Record isTop M := { }.
HB.structure Definition Top := {M of isTop M}.

HB.mixin Record isA1 M of Top M := { }.
HB.structure Definition A1 := {M of isA1 M & isTop M}.

HB.mixin Record isA2 M of Top M := { }.
HB.structure Definition A2 := {M of isA2 M & isTop M}.

HB.mixin Record isB1 M of A1 M := { }.
HB.structure Definition B1 := {M of isB1 M & }.

HB.mixin Record isB2 M of A2 M := { }.
HB.structure Definition B2 :=  {M of isB2 M & isA2 M }.

HB.structure Definition B2A1 := {M of B2 M & A1 M }.

HB.structure Definition A2B1 := {M of A2 M & B1 M }.

which corresponds to the following hiearchy:

that is lacking the following structure:

HB.structure Definition A1A2 := {M of isA1 M & isA2 M}.