From efa7e3596fa1209fc982e5678b9894e6cd35b031 Mon Sep 17 00:00:00 2001
From: Jason Gross <jasongross9@gmail.com>
Date: Sun, 8 Dec 2024 13:18:01 -0800
Subject: [PATCH] Apply suggestions from code review

---
 examples/run-example-048.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/examples/run-example-048.sh b/examples/run-example-048.sh
index 6da8ae8..2a2b9d5 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\|Corelib\)\.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\|Corelib\)\.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\.