Skip to content

Commit

Permalink
ProofGeneral#795, Compiler warnings: wrong usage of unescaped single …
Browse files Browse the repository at this point in the history
…quotes

coq/coq-db.el:31:11: Warning: defconst ‘coq-syntax-db’ docstring has wrong usage of unescaped single quotes

fixed
  • Loading branch information
andreas-roehler committed Oct 8, 2024
1 parent b30d65d commit 0e84b2b
Showing 1 changed file with 5 additions and 5 deletions.
10 changes: 5 additions & 5 deletions coq/coq-db.el
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ menu but only in interactive completions.
Example of what could be in your emacs init file:
\(defvar coq-user-tactics-db
'(
\\='(
(\"mytac\" \"mt\" \"mytac # #\" t \"mytac\")
(\"myassert by\" \"massb\" \"myassert ( # : # ) by #\" t \"assert\")
))
Expand Down Expand Up @@ -354,19 +354,19 @@ See `coq-syntax-db' for DB structure."

(defconst coq-solve-tactics-face 'coq-solve-tactics-face
"Expression that evaluates to a face.
Required so that 'coq-solve-tactics-face is a proper facename")
Required so that \\='coq-solve-tactics-face is a proper facename")

(defconst coq-cheat-face 'coq-cheat-face
"Expression that evaluates to a face.
Required so that 'coq-cheat-face is a proper facename")
Required so that \\='coq-cheat-face is a proper facename")

(defconst coq-symbol-binder-face 'coq-symbol-binder-face
"Expression that evaluates to a face.
Required so that 'coq-symbol-binder-face is a proper facename")
Required so that \\='coq-symbol-binder-face is a proper facename")

(defconst coq-symbol-face 'coq-symbol-face
"Expression that evaluates to a face.
Required so that 'coq-symbol-binder-face is a proper facename")
Required so that \\='coq-symbol-binder-face is a proper facename")

(defconst coq-question-mark-face 'coq-question-mark-face)

Expand Down

0 comments on commit 0e84b2b

Please sign in to comment.