Skip to content
Snippets Groups Projects
Commit a82eb791 authored by Ralf Jung's avatar Ralf Jung
Browse files

check for missing 'Hint Mode'

parent aeb449a7
No related tags found
No related merge requests found
......@@ -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
......@@ -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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment