Adapt to coq/coq#19530

JasonGross · Dec 7, 2024 · 27538d0 · 27538d0
1 parent 6f29d5f
commit 27538d0
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 6 deletions.
diff --git 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
@@ -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\.