diff options
| author | Jim Fehrle | 2020-10-15 00:03:29 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-10-15 00:03:29 -0700 |
| commit | 122cfabc4a453025b87ff599a12c09f988b300d6 (patch) | |
| tree | e08e76fdafb4877305de4bd2b1a560b9ded2439d | |
| parent | 411025844a4c005ce03d77c6c640807c28269d4a (diff) | |
Require at least one reference for Typeclasses Opaque/Transparent
(zero references is currently a no-op)
| -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 |