aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2018-06-01 09:57:52 +0200
committerGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2018-06-01 09:57:52 +0200
commit4441ce2d578633815bef4647711da8363ea68d85 (patch)
tree8ddc7b297e9947174a2c2586f4960559cc287243
parent31dda92a0bf190fd526e0a6d9502c197bdd08eb1 (diff)
Fixed a typo in previous commits.
-rw-r--r--coq/coq.el4
1 files changed, 2 insertions, 2 deletions
diff --git a/coq/coq.el b/coq/coq.el
index 50f0ebe6..52782fa9 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -2882,8 +2882,8 @@ number of hypothesis displayed, without hiding the goal"
(add-hook 'proof-shell-handle-delayed-output-hook
(lambda () (setq coq-hyps-positions (coq-detect-hyps proof-goals-buffer))
- (coq-highlight-selected-hyps))
- (coq-hide-hyps))
+ (coq-highlight-selected-hyps)
+ (coq-hide-hyps)))