Skip to content

Commit

Permalink
Apply suggestions from code review
Browse files Browse the repository at this point in the history
  • Loading branch information
JasonGross authored Dec 8, 2024
1 parent 27538d0 commit 8274140
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions examples/run-example-048.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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\.
Expand All @@ -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\.
Expand Down

0 comments on commit 8274140

Please sign in to comment.