From 616b4062f696b95fcb6e4d220cc3d261d9b1b7a8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 13 Jan 2021 18:19:48 +0100
Subject: [PATCH] ref tests: normalize subgoal to goal

---
 test-normalizer.sed  | 2 ++
 tests/telescopes.ref | 6 +++---
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/test-normalizer.sed b/test-normalizer.sed
index e69de29b..97b8c63c 100644
--- a/test-normalizer.sed
+++ b/test-normalizer.sed
@@ -0,0 +1,2 @@
+# adjust for https://github.com/coq/coq/pull/13656
+s/subgoal/goal/g
diff --git a/tests/telescopes.ref b/tests/telescopes.ref
index 485cc5c1..afac10f0 100644
--- a/tests/telescopes.ref
+++ b/tests/telescopes.ref
@@ -1,16 +1,16 @@
-1 subgoal
+1 goal
   
   X : tele
   α, β, γ1, γ2 : X → Prop
   ============================
   accessor α β γ1 → accessor α β (λ.. x : X, γ1 x ∨ γ2 x)
-1 subgoal
+1 goal
   
   X : tele
   α, β, γ1, γ2 : X → Prop
   ============================
   ∀.. x : X, γ1 x → (λ.. x0 : X, γ1 x0 ∨ γ2 x0) x
-1 subgoal
+1 goal
   
   X : tele
   α, β, γ1, γ2 : X → Prop
-- 
GitLab