From 122cfabc4a453025b87ff599a12c09f988b300d6 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Thu, 15 Oct 2020 00:03:29 -0700
Subject: Require at least one reference for Typeclasses Opaque/Transparent
 (zero references is currently a no-op)

---
 plugins/ltac/g_class.mlg | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 8d197e6056..21d1782fce 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -31,12 +31,12 @@ let set_transparency cl b =
 }
 
 VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings CLASSIFIED AS SIDEFF
-| [ "Typeclasses" "Transparent" reference_list(cl) ] -> {
+| [ "Typeclasses" "Transparent" ne_reference_list(cl) ] -> {
     set_transparency cl true }
 END
 
 VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings CLASSIFIED AS SIDEFF
-| [ "Typeclasses" "Opaque" reference_list(cl) ] -> {
+| [ "Typeclasses" "Opaque" ne_reference_list(cl) ] -> {
     set_transparency cl false }
 END
 
-- 
cgit v1.2.3