From ac73a491893f152c97f44e13109d124e46ab70b0 Mon Sep 17 00:00:00 2001
From: Dario Halilovic <dario.halilovic@epfl.ch>
Date: Wed, 16 Sep 2026 16:17:13 +0200
Subject: [PATCH] fix: use toplevel module name in errors when using
 ProofGeneral

---
 src/snippet.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/snippet.ml b/src/snippet.ml
index 1aed569..86a837c 100644
--- a/src/snippet.ml
+++ b/src/snippet.ml
@@ -1,5 +1,7 @@
 (** Representation of OCaml code snippets. *)
 
+open Names
+
 (** {1 Snippets} *)
 
 type t =
@@ -93,8 +95,12 @@ module Scaffold = struct
     let file =
       match loc.fname with
       | ToplevelInput ->
-         (* FIXME: Obtain original file name under ProofGeneral's toplevel. *)
-         "_toplevel_"
+         (* Use the module name set by the [-top] option, if any. *)
+         let _, top_module_name = Libnames.split_dirpath (Lib.library_dp ()) in
+         begin match Id.to_string top_module_name with
+         | "Top" (* default *) -> "_toplevel_"
+         | name -> name ^ ".v"
+         end
       | InFile { file; _ } -> file
     in
     add_line_number_directive ~line:loc.line_nb ~file scaffold;