diff options
| author | coqbot-app[bot] | 2020-10-19 11:55:55 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-19 11:55:55 +0000 |
| commit | 6ac6f430b75b74a7361f03be35bce670cb380d03 (patch) | |
| tree | a1a444695baf43a312c648319ddd289d4c12ce17 /plugins/ltac | |
| parent | 3690c28e1acbd4a689f072967117f6d7455c428e (diff) | |
| parent | 122cfabc4a453025b87ff599a12c09f988b300d6 (diff) | |
Merge PR #13197: Require at least one reference for Typeclasses Opaque/Transparent
Reviewed-by: SkySkimmer
Diffstat (limited to 'plugins/ltac')
| -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 a86045b0a4..8c2e633be5 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 |