From 3da2dbe9728ae7f5b1860a8e3a6c458e6d976f84 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Thu, 17 Dec 2020 15:04:36 -0800
Subject: Avoid using "subgoals" in the UI, it means the same as "goals"

---
 test-suite/output/CompactContexts.out | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite/output/CompactContexts.out')

diff --git a/test-suite/output/CompactContexts.out b/test-suite/output/CompactContexts.out
index 9d1d19877e..f0a8019b67 100644
--- a/test-suite/output/CompactContexts.out
+++ b/test-suite/output/CompactContexts.out
@@ -1,4 +1,4 @@
-1 subgoal
+1 goal
   
   hP1 : True
   a : nat   b : list nat   h : forall x : nat, {y : nat | y > x}
-- 
cgit v1.2.3