Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion ci/compile-tests/007-slow-require/runtest.el
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,7 @@ See `cct-generic-check-main-buffer'."
(defun test-slow-require (n)
"Test part N of slow require job tests.
XXX Test a setting where the second require job is still in state
'enqueued-coqdep when the first one finishes."
\\+`enqueued-coqdep' when the first one finishes."
(let*
;; .v file names are used as file and as buffer names
((av (format "a%d.v" n))
Expand Down
12 changes: 6 additions & 6 deletions ci/compile-tests/cct-lib.el
Original file line number Diff line number Diff line change
Expand Up @@ -42,10 +42,10 @@
"Set to t to get more output during test runs.")

(defvar cct-before-busy-waiting-hook nil
"Hooks run by cct-process-to-line before busy waiting.")
"Hooks run by `cct-process-to-line' before busy waiting.")

(defvar cct-after-busy-waiting-hook nil
"Hooks run by cct-process-to-line after busy waiting.")
"Hooks run by `cct-process-to-line' after busy waiting.")


(defmacro cct-implies (p q)
Expand Down Expand Up @@ -165,7 +165,7 @@ Runs `cct-before-busy-waiting-hook' and
PG uses a number of overlapping and non-overlapping spans (read
overlays) in the asserted and queue region of the proof buffer,
see the comments in generic/proof-script.el. Spans of type
vanilla (stored at 'type in the span property list) are created
vanilla (stored at \\+`type' in the span property list) are created
for real commands (not for comments). They hold various
information that is used, among others, for backtracking.

Expand All @@ -188,7 +188,7 @@ and `current-message' does not return anything."

(defun cct-check-locked (line locked-state)
"Check that line LINE has locked state LOCKED-STATE.
LOCKED-STATE must be 'locked or 'unlocked. This function checks
LOCKED-STATE must be \\+`locked' or \\+`unlocked'. This function checks
whether line LINE is inside or outside the asserted (locked)
region of the buffer and signals a test failure if not."
(let ((locked (eq locked-state 'locked)))
Expand Down Expand Up @@ -219,7 +219,7 @@ region of the buffer and signals a test failure if not."

(defun cct-check-files-locked (line lock-state files)
"Check that all FILES at line number LINE have lock state LOCK-STATE.
LOCK-STATE must be either 'locked or 'unlocked. FILES must be
LOCK-STATE must be either \\+`locked' or \\+`unlocked'. FILES must be
list of file names."
(when cct--debug-tests
(message "check files %s at line %d: %s"
Expand All @@ -236,7 +236,7 @@ list of file names."
The comparison treats ANCESTORS as set but the file names must
be `equal' as strings.

Ancestors are recorded in the 'coq-locked-ancestors property of
Ancestors are recorded in the \\+`coq-locked-ancestors' property of
the vanilla spans of require commands, see the in-file
documentation of coq/coq-par-compile.el."
(let ((locked-ancestors
Expand Down
28 changes: 14 additions & 14 deletions coq/coq-compile-common.el
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,7 @@ Must be used together with `coq-par-enable'."


(defun coq-switch-compilation-method ()
"Set function for function coq-compile-parallel-in-background."
"Set function for function `coq-compile-parallel-in-background'."
(if coq-compile-parallel-in-background
(progn
(coq-par-enable)
Expand Down Expand Up @@ -125,14 +125,14 @@ This is the internal value, use

(defun coq-max-second-stage-setter (symbol new-value)
":set function for `coq-max-background-second-stage-percentage'.
SYMBOL should be \\='coq-max-background-second-stage-percentage"
SYMBOL should be \\=`coq-max-background-second-stage-percentage'"
(set-default symbol new-value)
(setq coq--max-background-second-stage-percentage-shadow new-value)
(coq-set-max-second-stage-jobs))

(defun coq-max-jobs-setter (symbol new-value)
":set function for `coq-max-background-compilation-jobs'.
SYMBOL should be \\='coq-max-background-compilation-jobs"
SYMBOL should be \\=`coq-max-background-compilation-jobs'"
(set-default symbol new-value)
(cond
((eq new-value 'all-cpus)
Expand Down Expand Up @@ -342,7 +342,7 @@ This option can be set/reset via menu
(defcustom coq-max-background-compilation-jobs 'all-cpus
"Maximal number of parallel jobs, if parallel compilation is enabled.
Use the number of available CPU cores if this is set to
\\='all-cpus. This variable is the user setting. The value that is
\\=`all-cpus'. This variable is the user setting. The value that is
really used is `coq--internal-max-jobs'. Use `coq-max-jobs-setter'
or the customization system to change this variable. Otherwise
your change will have no effect, because `coq--internal-max-jobs'
Expand Down Expand Up @@ -387,7 +387,7 @@ the ``-vok'' second stage was implemented."
"Delay in seconds before starting the second stage compilation.
The delay is applied to both ``-vok'' and vio2vo second stages.
For Coq < 8.11 and vio2vo delay helps to avoid running into a
library inconsistency with \\='quick-and-vio2vo, see Coq issue
library inconsistency with \\+`quick-and-vio2vo', see Coq issue
#5223.

For backward compatibility, if this option is not customized, it
Expand Down Expand Up @@ -464,8 +464,8 @@ it might be a string, or one of the symbols `physical-dir',
`module-object', `module-source', `qualified-id' and
`requiring-file', which are bound to, respectively, the physical
directory containing the source file, the Coq object file in
\\='physical-dir that will be loaded, the Coq source file in
\\='physical-dir whose object will be loaded, the qualified module
\\+`physical-dir' that will be loaded, the Coq source file in
\\+`physical-dir' whose object will be loaded, the qualified module
identifier that occurs in the \"Require\" command, and the file
that contains the \"Require\".")

Expand All @@ -477,10 +477,10 @@ buffers, where Coq buffers means all buffers in Coq mode except the current
buffer. Secondly, Emacs can ask about each such buffer or save all of them
unconditionally.

This makes four permitted values: \\='ask-coq to confirm saving all
modified Coq buffers, \\='ask-all to confirm saving all modified
buffers, \\='save-coq to save all modified Coq buffers without
confirmation and \\='save-all to save all modified buffers without
This makes four permitted values: \\+`ask-coq' to confirm saving all
modified Coq buffers, \\+`ask-all' to confirm saving all modified
buffers, \\+`save-coq' to save all modified Coq buffers without
confirmation and \\+`save-all' to save all modified buffers without
confirmation.

This option can be set via menu
Expand Down Expand Up @@ -607,9 +607,9 @@ the second low the lower 16 bits of the time."
(defun coq-max-dep-mod-time (dep-mod-times)
"Return the maximum in DEP-MOD-TIMES.
Argument DEP-MOD-TIMES is a list where each element is either a
time value (see `time-less-or-equal') or \\='just-compiled. The
time value (see `time-less-or-equal') or \\+`just-compiled'. The
function returns the maximum of the elements in DEP-MOD-TIMES,
where \\='just-compiled is considered the greatest time value. If
where \\+`just-compiled' is considered the greatest time value. If
DEP-MOD-TIMES is empty it returns nil."
(let ((max nil))
(while dep-mod-times
Expand Down Expand Up @@ -808,7 +808,7 @@ not backed by a file. The buffer to test must be current."

(defun coq-compile-save-some-buffers ()
"Save buffers according to `coq-compile-auto-save'.
Uses the local variable coq-compile-buffer-with-current-require to pass the
Uses the local variable `coq-compile-buffer-with-current-require' to pass the
current buffer (which contains the Require command) to
`coq-compile-save-buffer-filter'."
(let ((coq-compile-buffer-with-current-require (current-buffer))
Expand Down
8 changes: 4 additions & 4 deletions coq/coq-db.el
Original file line number Diff line number Diff line change
Expand Up @@ -388,19 +388,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
4 changes: 2 additions & 2 deletions coq/coq-indent.el
Original file line number Diff line number Diff line change
Expand Up @@ -695,7 +695,7 @@ The point is put exactly before first non comment letter of the command."
;; (defun coq-find-unopened (&optional optlvl limit)
;; "Find the last unopened close item (looking forward from point).
;; Counter starts to OPTLVL (default 1) and stops when reaching
;; LIMIT (default point-max). This function only works inside an
;; LIMIT (default `point-max'). This function only works inside an
;; expression."

;; (let ((lvl (or optlvl 1)) after nextpt endpt)
Expand Down Expand Up @@ -751,7 +751,7 @@ The point is put exactly before first non comment letter of the command."

;; (defun coq-end-offset (&optional limit)
;; "Find the first unclosed open indent item, and return its column.
;; Stop when reaching LIMIT (default to point-min)."
;; Stop when reaching LIMIT (default to `point-min')."
;; (save-excursion
;; (let ((found nil)
;; (anyreg (proof-regexp-alt "\\`" proof-indent-any-regexp)))
Expand Down
4 changes: 2 additions & 2 deletions coq/coq-local-vars.el
Original file line number Diff line number Diff line change
Expand Up @@ -50,8 +50,8 @@ coqtop -foo3 -R foo bar -I foo2
FILE VARIABLES

If for some reason you want to avoid or override the project file
method, you can use the file variables. See Info node (emacs)File
Variables. This feature of Emacs allows to set Emacs variables on a
method, you can use the file variables. See Info node `(emacs)File
Variables'. This feature of Emacs allows to set Emacs variables on a
per-file basis. File Variables are (usually) written as a list at the
end of the file.

Expand Down
2 changes: 1 addition & 1 deletion coq/coq-mode.el
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ instead of just \"coqtop\".
This must be a single program name with no arguments. See option
`coq-prog-args' to manually adjust the arguments to the Coq process.
See also `coq-prog-env' to adjust the environment.
With then 2025 new CLI \\='rocq\\=', this command only return \\='rocq\\='."
With then 2025 new CLI \\+`rocq', this command only return \\+`rocq'."
:type 'string
:group 'coq
:group 'coq-mode)
Expand Down
Loading
Loading