Fixed some obvious issues in Emacs related files

HOL-Theorem-Prover · Sep 23, 2024 · 0ee9368 · 0ee9368
1 parent 8094199
commit 0ee9368
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/tools/hol-input.el b/tools/hol-input.el
@@ -190,7 +190,7 @@ order for the change to take effect."
                        (sexp :tag "Tweaking function"))))
 
 (defcustom hol-input-translations
-  (eval-when-compile (setq-local max-lisp-eval-depth 2800) `(
+  (eval-when-compile (setq-local max-lisp-eval-depth 3200) `(
 
   ;; Negation
 

diff --git a/tools/holscript-mode.el b/tools/holscript-mode.el
@@ -152,11 +152,11 @@ On existing quotes, toggles between ‘-’ and “-” pairs.  Otherwise, inser
            (setq n (- n 1))))
         ((< n 0)
          (setq n (- n))
-         (setq n (- n (if (equal (skip-syntax-backward ".") 0) 0 1))))
+         (setq n (- n (if (equal (skip-syntax-backward ".") 0) 0 1)))
          (while (> n 0)
            (skip-syntax-backward "^.")
            (skip-syntax-backward ".")
-           (setq n (- n 1)))))
+           (setq n (- n 1))))))
 
 (defun is-a-then (s)
   (and s (or (string-equal s "THEN")