diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2016-01-27 17:55:02 +0100 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2016-01-27 17:55:02 +0100 |
| commit | 626013259652e208ce99c84463e05ce22e62484a (patch) | |
| tree | 1c202419e91b62dd5c43a2e12fc38c35c5ba6883 | |
| parent | d35b46774617b44776730adf9d8ea4807a75e8a2 (diff) | |
Fixed recent coq syntax change (tac !H become tac (H)).
| -rw-r--r-- | coq/coq.el | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -2047,7 +2047,7 @@ Warning: this makes the error messages (and location) wrong.") (cond ((string-match ";" s) s) ;; composed tactic cannot be treated ((string-match coq-auto-as-hack-hyp-name-regex s) - (concat "infoH " (match-string 1 s) " !" (match-string 2 s) ".")) + (concat "infoH " (match-string 1 s) " (" (match-string 2 s) ").")) ((string-match coq-keywords-accepting-as-regex s) (concat "infoH " s)) (t (concat "infoH " s)))) |