Adapt to rocq-prover/rocq#19530 (#240)

* Adapt to rocq-prover/rocq#19530

* Apply suggestions from code review

---------

Co-authored-by: Jason Gross <jasongross9@gmail.com>

Author: proux01

coq_tools/find_bug.py

@@ -2244,11 +2244,16 @@ def make_make_coqc(coqc_prog, **kwargs):
                 coqpath_path = os.environ.get('COQPATH', '')
                 coqpath_paths = coqpath_path.split(os.pathsep) if coqpath_path else []
                 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(

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\|Stdlib\)\.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\|Stdlib\)\.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\.