diff --git a/tests/err_instance_nop.v.out.2 b/tests/err_instance_nop.v.out.2 new file mode 100644 index 00000000..7a94d24c --- /dev/null +++ b/tests/err_instance_nop.v.out.2 @@ -0,0 +1,5 @@ +Toplevel input, characters 0-48: +> HB.instance Definition _ : M nat := M.Build nat. +> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] diff --git a/tests/err_miss_dep.v.out.2 b/tests/err_miss_dep.v.out.2 new file mode 100644 index 00000000..493069f1 --- /dev/null +++ b/tests/err_miss_dep.v.out.2 @@ -0,0 +1,9 @@ +Toplevel input, characters 0-62: +> HB.structure Definition AbelianGrp := { A of IsAbelianGrp A }. +> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Warning: +pulling in dependencies: [err_miss_dep_IsAddComoid] +Please list them or end the declaration with '&' +[HB.implicit-structure-dependency,HB,elpi,default] +The command has indeed failed with message: +HB: Unable to find mixin err_miss_dep_IsAddComoid on subject K diff --git a/tests/missing_join_error.v.out.2 b/tests/missing_join_error.v.out.2 new file mode 100644 index 00000000..0fc8407a --- /dev/null +++ b/tests/missing_join_error.v.out.2 @@ -0,0 +1,12 @@ +Toplevel input, characters 0-55: +> HB.structure Definition B2 := {M of isB2 M & isA2 M }. +> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Warning: +pulling in dependencies: [missing_join_error_isTop] +Please list them or end the declaration with '&' +[HB.implicit-structure-dependency,HB,elpi,default] +The command has indeed failed with message: +You must declare the hierarchy bottom-up or add a missing join. +There are two ways out: +- declare structure A2B1 before structure B2A1 if B2A1 inherits from it; +- declare an additional structure that inherits from both A1 and A2 and from which A2B1 and/or B2A1 inherit.