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

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