diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2016-05-20 09:48:13 +0200 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2016-05-20 09:48:13 +0200 |
| commit | 6590f705000ec0a6e0260552b48300c65aa83153 (patch) | |
| tree | 9d655ed80e1d0ae42f7f83e99df4e6ce5addef05 /coq/coq.el | |
| parent | 9ae103b86dd3cdfc3e6e6326ebc1a8f803e50f7d (diff) | |
Fix #72+ make user keywords prioritized over default ones.
Diffstat (limited to 'coq/coq.el')
| -rw-r--r-- | coq/coq.el | 9 |
1 files changed, 4 insertions, 5 deletions
@@ -1328,11 +1328,10 @@ goal is redisplayed." (let* ((id (coq-id-or-notation-at-point)) (re (regexp-quote (or id "")))) (when coq-highlight-id-last-regexp - (coq-unhighlight-id-in-goals coq-highlight-id-last-regexp) - (if (equal id coq-highlight-id-last-regexp) - (setq coq-highlight-id-last-regexp "") - (coq-highlight-id-in-goals re) - (setq coq-highlight-id-last-regexp re))))) + (coq-unhighlight-id-in-goals coq-highlight-id-last-regexp)) + (coq-highlight-id-in-goals re) + (setq coq-highlight-id-last-regexp re))) + (proof-definvisible coq-PrintHint "Print Hint. ") |