diff --git a/coq-lint.sh b/coq-lint.sh
index 18a36adeaea3cf6b314264e871d4270d89c46d9f..b849dacc679ea0a3ff94407b8d51bc93a96b4f67 100755
--- a/coq-lint.sh
+++ b/coq-lint.sh
@@ -10,3 +10,10 @@ if egrep -n '^\s*((Existing\s+|Program\s+)Instance|Arguments|Remove|Hint\s+(Exte
     echo
     exit 1
 fi
+
+for CLASS in $(egrep -v 'coq-lint-ignore' "$FILE" | egrep 'Class +[^ ]+\b' -o | tr -s ' ' | cut -f 2 -d ' '); do
+    if ! egrep "Global +Hint +Mode +$CLASS +" "$FILE" -q; then
+        echo "No 'Global Hint Mode' for class '$CLASS'"
+        exit 1
+    fi
+done
diff --git a/theories/base.v b/theories/base.v
index df49b47de9e9bb1c89b34669386330bcefcffbb2..8184136a74850472a0af522eb90743163f23d755 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -98,8 +98,8 @@ Global Arguments tc_opaque {_} _ /.
 important to note that we duplicate the definitions, and do not declare the
 existing logical operators as type classes. That is, we do not say:
 
-  Existing Class or.
-  Existing Class and.
+  Existing Class or.    (* coq-lint-ignore *)
+  Existing Class and.   (* coq-lint-ignore *)
 
 If we could define the existing logical operators as classes, there is no way
 of disambiguating whether a premise of a lemma should be solved by type class