From fd8f6c5235f400df4f60a1d55b4a5db4180c07e9 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Wed, 13 Oct 2021 13:34:57 -0400
Subject: [PATCH] Normalize focused goal output

Merge the "1 focused goal" line with the subsequent "(shelved: 1)" line,
since this is the new output in Coq 8.15+.

Iris does not currently produce this output, since no test calls `Show`
with shelved goals, but this future-proofs the test normalization.
---
 test-normalizer.sed | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/test-normalizer.sed b/test-normalizer.sed
index ca19aad59..5da5d6fbc 100644
--- a/test-normalizer.sed
+++ b/test-normalizer.sed
@@ -2,3 +2,5 @@
 s/(simple_intropattern)/(intropattern)/g
 # adjust for https://github.com/coq/coq/pull/13656
 s/subgoal/goal/g
+# merge with subsequent line for https://github.com/coq/coq/pull/14999
+/[0-9]* focused goals\?$/{N;s/\n */ /;}
-- 
GitLab