diff options
| -rw-r--r-- | plugins/ltac/g_class.mlg | 4 |
1 files changed, 2 insertions, 2 deletions
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 |