         (set-process-sentinel (get-buffer-process (current-buffer))
                               #'ocamldebug-sentinel)
         (ocamldebug-mode)))
-  (ocamldebug-set-buffer)))
+    (ocamldebug-set-buffer)
+    (insert "source dune_db_409")))
+
+;; Provide correct breakpoint setting in dune wrapped libraries
+;; (assuming only 1 library/dune file)
+(defun coqdev--read-from-file (file)
+  "Read FILE as a list of sexps. If invalid syntax, return nil and message the error."
+  (with-temp-buffer
+    (save-excursion
+      (insert "(\n")
+      (insert-file-contents file)
+      (goto-char (point-max))
+      (insert "\n)\n"))
+    (condition-case err
+        (read (current-buffer))
+      ((error err) (progn (message "Error reading file %S: %S" file err) nil)))))
+
+(defun coqdev--find-single-library (sexps)
+  "If list SEXPS has an element whose `car' is \"library\", return the first one.
+Otherwise return `nil'."
+  (let ((libs (seq-filter (lambda (elt) (equal (car elt) 'library)) sexps)))
+    (and libs (car libs))))
+
+(defun coqdev--dune-library-name (lib)
+  "With LIB a dune-syntax library stanza, get its name as a string."
+  (let ((field (or (seq-find (lambda (field) (and (consp field) (equal (car field) 'name))) lib)
+                   (seq-find (lambda (field) (and (consp field) (equal (car field) 'public\_name))) lib))))
+    (symbol-name (car (cdr field)))))
+
+(defun coqdev--upcase-first-char (arg)
+  "Set the first character of ARG to uppercase."
+  (concat (upcase (substring arg 0 1)) (substring arg 1 (length arg))))
+
+(defun coqdev--real-module-name (filename)
+  "Return module name for ocamldebug, taking into account dune wrapping.
+(for now only understands dune files with a single library stanza)"
+  (let ((mod (substring filename (string-match "\\([^/]*\\)\\.ml$" filename) (match-end 1)))
+        (dune (concat (file-name-directory filename) "dune")))
+    (if (file-exists-p dune)
+        (if-let* ((contents (coqdev--read-from-file dune))
+                  (lib (coqdev--find-single-library contents))
+                  (is-wrapped (null (seq-contains-p lib '(wrapped false))))
+                  (libname (coqdev--dune-library-name lib)))
+            (concat libname "__" (coqdev--upcase-first-char mod))
+          mod)
+      mod)))
+
+(with-eval-after-load 'ocamldebug
+  (defun ocamldebug-module-name (arg)
+    (coqdev--real-module-name arg)))
 
 ;; This Elisp snippet adds a regexp parser for the format of Anomaly
 ;; backtraces (coqc -bt ...), to the error parser of the Compilation


;;; Code:

(defun coqdev-default-directory ()
  "Return the Coq repository containing `default-directory'."
  (let ((dir (locate-dominating-file default-directory "coq-core.opam")))
    (when dir (expand-file-name dir))))

(defun coqdev-setup-compile-command ()
  "Setup `compile-command' for Coq development."
  (let ((dir (coqdev-default-directory)))
    ;; we add a space at the end to make it easy to add arguments (eg -j or target)
    (when dir (setq-local compile-command (concat "make -C " (shell-quote-argument dir) " ")))))
(add-hook 'hack-local-variables-hook #'coqdev-setup-compile-command)

(defvar camldebug-command-name) ; from camldebug.el (caml package)

      (setq-local coq-prog-name (concat dir "_build/default/dev/shim/coqtop-prelude")))))
(add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral)

(defvar coqdev-ocamldebug-command "dune exec -- dev/dune-dbg coqc /tmp/foo.v"
  "Command run by `coqdev-ocamldebug'")

(declare-function comint-check-proc "comint")
(declare-function tuareg--split-args "tuareg")
(declare-function ocamldebug-filter "ocamldebug")
(declare-function ocamldebug-sentinel "ocamldebug")
(declare-function ocamldebug-mode "ocamldebug")
(declare-function ocamldebug-set-buffer "ocamldebug")
(defun coqdev-ocamldebug ()
  "Runs a command in an ocamldebug buffer."
  (interactive)
  (require 'ocamldebug)
  (let* ((dir (read-directory-name "Run from directory: "
                                   (coqdev-default-directory)))
         (name "ocamldebug-coq")
