From a82eb79140ed07020afdc151fab8298f93dd0a62 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 3 Jun 2021 18:15:14 +0200
Subject: [PATCH] check for missing 'Hint Mode'
---
coq-lint.sh | 7 +++++++
theories/base.v | 4 ++--
2 files changed, 9 insertions(+), 2 deletions(-)
diff --git a/coq-lint.sh b/coq-lint.sh
index 18a36ade..b849dacc 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 df49b47d..8184136a 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
--
GitLab