From 23d1894070665058d4af14295c8fe7e1d4db3957 Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cohen@crans.org>
Date: Fri, 13 Dec 2024 14:16:59 +0100
Subject: [PATCH] new warning output diff

---
 tests/err_miss_dep.v.out | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/tests/err_miss_dep.v.out b/tests/err_miss_dep.v.out
index 32784f55..431d23c9 100644
--- 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