From 400f7184d113159208ebe97a61f02cbf9625140d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 16 Dec 2024 12:55:11 +0100 Subject: [PATCH] Stdlib.All use separate Require commands That way when we get an error or warning we can see which Require produced it by looking at the generated file. --- stdlib/tools/gen_all.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/stdlib/tools/gen_all.ml b/stdlib/tools/gen_all.ml index 89bf37cab0e6..bf070d95a955 100644 --- a/stdlib/tools/gen_all.ml +++ b/stdlib/tools/gen_all.ml @@ -12,8 +12,6 @@ let from = "Stdlib" let () = Printf.printf "Set Warnings \"-deprecated-library-file,-warn-library-file\".\n\n" -let () = Printf.printf "From %s Require\n" from - let logical_concat prefix f = let f = Filename.remove_extension f in match prefix with @@ -40,7 +38,7 @@ let rec traverse todo todo' = match todo, todo' with let () = if Filename.extension path = ".v" && logical <> "All" - then Printf.printf " %s\n" logical + then Printf.printf "From %s Require Export %s.\n" from logical in todo' | _ -> todo' @@ -49,4 +47,4 @@ let rec traverse todo todo' = match todo, todo' with let () = traverse [".", ""] [] -let () = Printf.printf ".\n%!" +let () = Printf.printf "%!"