From 3c9908f9b7c73af2ad9c617b3ced424dca2fcb2e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 14 Nov 2020 20:47:21 +0100
Subject: Fix test-suite.

---
 test-suite/output/TypeclassDebug.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/test-suite/output/TypeclassDebug.v b/test-suite/output/TypeclassDebug.v
index 2e4008ae56..0bd3d5fa40 100644
--- a/test-suite/output/TypeclassDebug.v
+++ b/test-suite/output/TypeclassDebug.v
@@ -2,6 +2,7 @@
 
 Parameter foo : Prop.
 Axiom H : foo -> foo.
+#[global]
 Hint Resolve H : foo.
 Goal foo.
 Typeclasses eauto := debug.
-- 
cgit v1.2.3