diff options
| author | Pierre Courtieu | 2020-04-16 15:51:15 +0200 |
|---|---|---|
| committer | Pierre Courtieu | 2020-04-16 15:51:15 +0200 |
| commit | 18311b7cc64bbe2b271a45d72b4ba2affa5213bd (patch) | |
| tree | 5fb3d0b90e3db3821b226eca0ca9774cbe6332ca /generic | |
| parent | 017d4b516713622a160eb6786c2bde5f7f6ee91e (diff) | |
Fix hide/show proof.
Bug described by @MdeLv at:
https://github.com/coq/coq/issues/12088#issuecomment-613266520
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/pg-user.el | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el index d2259ef8..f10f02c1 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -770,7 +770,7 @@ If NUM is negative, move upwards. Return new span." (list (pg-span-name span)) (list (vector "Show/hide" - (if idiom (list 'pg-toggle-element-visibility (quote idiom) name)) + (if idiom (list 'pg-toggle-element-visibility `(quote ,idiom) name)) (not (not idiom)))) (list (vector "Copy" (list 'pg-copy-span-contents span) t)) |