   (define-key fstar-mode-map (kbd "C-c C-n") #'fstar-subp-advance-next)
   (define-key fstar-mode-map (kbd "C-c C-u") #'fstar-subp-retract-last)
   (define-key fstar-mode-map (kbd "C-c C-p") #'fstar-subp-retract-last)
-  (define-key fstar-mode-map (kbd "C-c <C-return>") #'fstar-subp-advance-or-retract-to-point))
+  (define-key fstar-mode-map (kbd "C-c <C-return>") #'fstar-subp-advance-or-retract-to-point)
+  (flycheck-mode -1))
 
 ;;; Comment syntax
 

If NO-ERROR is set, do not report an error if the region is empty."
  (let ((beg (fstar-subp-unprocessed-beginning))
        (end (fstar-skip-spaces-backwards-from end)))
    (assert (cl-loop for overlay in (overlays-in beg end)
                     never (fstar-subp-tracking-overlay-p overlay)))
    (if (<= end beg)
        (unless no-error

(defun fstar-setup-indentation ()
  "Setup indentation for F*."
  (setq-local indent-line-function #'fstar-indent)
  (when (fboundp 'electric-indent-local-mode)
    (electric-indent-local-mode -1)))

;;; Interaction with the server (interactive mode)

