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"

---
 tools/coqdoc/output.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 10edb0b4db..50aa658128 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -48,7 +48,7 @@ let is_keyword =
       "Delimit"; "Bind"; "Open"; "Scope"; "Inline";
       "Implicit Arguments"; "Add"; "Strict";
       "Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation";
-      "subgoal"; "subgoals"; "vm_compute";
+      "goal"; "goals"; "vm_compute";
       "Opaque"; "Transparent"; "Time";
       "Extraction"; "Extract";
       "Variant";
-- 
cgit v1.2.3