new warning output diff

math-comp · Dec 13, 2024 · 23d1894 · 23d1894
1 parent b497a7e
commit 23d1894
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/tests/err_miss_dep.v.out b/tests/err_miss_dep.v.out
@@ -1,2 +1,9 @@
+Toplevel input, character 0:
+> 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