From 27538d0ee76ec69e03bc7896942c9c26d7d179c9 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Tue, 3 Dec 2024 14:48:11 +0100
Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/19530

---
 coq_tools/find_bug.py       | 13 +++++++++----
 examples/run-example-048.sh |  4 ++--
 2 files changed, 11 insertions(+), 6 deletions(-)

diff --git a/coq_tools/find_bug.py b/coq_tools/find_bug.py
index 569face..79aa568 100755
--- a/coq_tools/find_bug.py
+++ b/coq_tools/find_bug.py
@@ -2243,11 +2243,16 @@ def make_make_coqc(coqc_prog, **kwargs):
                 coq_user_contrib_path = os.path.join(os.path.join(coq_lib_path, "user-contrib"), "Stdlib")
                 coqpath_paths = os.environ.get('COQPATH', '').split(os.pathsep)
                 if args.inline_coqlib:
+                    if coqc_version != "" and coqc_version[0] == '8':
+                        env[passing_prefix + "libnames"] = tuple(
+                            list(env[passing_prefix + "libnames"]) + [(coq_theories_path, "Coq")]
+                        )
+                    else:
+                        env[passing_prefix + "libnames"] = tuple(
+                            list(env[passing_prefix + "libnames"]) + [(coq_theories_path, "Corelib")]
+                        )
                     env[passing_prefix + "libnames"] = tuple(
-                        list(env[passing_prefix + "libnames"]) + [(coq_theories_path, "Coq")]
-                    )
-                    env[passing_prefix + "libnames"] = tuple(
-                        list(env[passing_prefix + "libnames"]) + [(coq_user_contrib_path, "Coq")]
+                        list(env[passing_prefix + "libnames"]) + [(coq_user_contrib_path, "Stdlib")]
                     )
                     for p in coqpath_paths:
                         env[passing_prefix + "libnames"] = tuple(
diff --git a/examples/run-example-048.sh b/examples/run-example-048.sh
index e2c775c..6da8ae8 100755
--- a/examples/run-example-048.sh
+++ b/examples/run-example-048.sh
@@ -89,7 +89,7 @@ find_bug "$EXAMPLE_INPUT" "$EXAMPLE_OUTPUT" "${EXTRA_ARGS[@]}" || exit $?
 (\* -\*- mode: coq; coq-prog-args: ([^)]*) -\*- \*)
 (\* File reduced by coq-bug-minimizer from original input, then from [0-9]\+ lines to [0-9]\+ lines, then from [0-9]\+ lines to [0-9]\+ lines, then from [0-9]\+ lines to [0-9]\+ lines, then from [0-9]\+ lines to [0-9]\+ lines \*)
 (\* coqc version [^\*]*\*)
-Require \(Coq\|Stdlib\)\.Init\.Ltac\.
+Require \(Coq\|Corelib\)\.Init\.Ltac\.
 
 Inductive False : Prop := \.
 Axiom proof_admitted : False\.
@@ -100,7 +100,7 @@ Global Set Universe Polymorphism\.
 Definition foo@{i} := Type@{i}\.
 
 End Foo\.
-\(Import \(Coq\|Stdlib\)\.Init\.Ltac\.
+\(Import \(Coq\|Corelib\)\.Init\.Ltac\.
 \)\?Monomorphic Inductive eq {A} (x : A) : forall _ : A, Prop := eq_refl : eq x x\.
 Arguments eq_refl {A x} , \[A\] x\.
 Definition foo@{} : Set\.