search

math-comp / hierarchy-builder

High level commands to declare a hierarchy based on packed classes
MIT License
95 stars 20 forks source link

Importing Order.TTheory in the middle break the code #407

Open hivert opened 9 months ago

hivert commented 9 months ago

The following code

From HB Require Import structures.
From mathcomp Require Import all_ssreflect.

Structure foo : Type := Foo {fooval :> seq nat; _ : size fooval == 1}.
HB.instance Definition _ := [isSub of foo for fooval].
HB.instance Definition _ := [Equality of foo by <:].

Import Order.TTheory.   (* HERE *)

Structure bar : Type := Bar {barval :> seq nat; _ : size barval == 0}.
HB.instance Definition _ := [isSub of bar for barval].
HB.instance Definition _ := [Equality of bar by <:].

Fails on the last line with

 Error: eqtype_Equality__to__eqtype_hasDecEq already exists.

On the other hand, if the import of Order.TTheory is before the declaration of foo or not here at all, everything works.

According to @CohenCyril on zulip : this is a bug in the seeded/random name generator.