aboutsummaryrefslogtreecommitdiffhomepage
path: root/easycrypt/easycrypt-hooks.el
diff options
context:
space:
mode:
authorGravatar Erik Martin-Dorel <erik@martin-dorel.org>2018-08-23 00:01:12 +0200
committerGravatar Erik Martin-Dorel <erik@martin-dorel.org>2018-08-23 01:23:31 +0200
commit86d22428959a0f5aecef270e0f4dd7d4b5712fc3 (patch)
tree676fe59b7644498172f96b6da605745a6bf71a13 /easycrypt/easycrypt-hooks.el
parent3ba86af3271111cb056676c631b7caa6897e06f1 (diff)
Fix most doc issues raised by (checkdoc)
Diffstat (limited to 'easycrypt/easycrypt-hooks.el')
-rw-r--r--easycrypt/easycrypt-hooks.el11
1 files changed, 10 insertions, 1 deletions
diff --git a/easycrypt/easycrypt-hooks.el b/easycrypt/easycrypt-hooks.el
index 3cf891e3..67592973 100644
--- a/easycrypt/easycrypt-hooks.el
+++ b/easycrypt/easycrypt-hooks.el
@@ -1,3 +1,5 @@
+;;; easycrypt-hooks.el --- Auxiliary functions for EasyCrypt mode
+
;; --------------------------------------------------------------------
;; Copyright (c) - 2012--2016 - IMDEA Software Institute
;; Copyright (c) - 2012--2016 - Inria
@@ -5,9 +7,14 @@
;; Distributed under the terms of the GPL-v3 license
;; --------------------------------------------------------------------
+;;; Commentary:
+;;
+
(require 'span)
(require 'proof)
+;;; Code:
+
(defvar easycrypt-last-but-one-statenum 0)
(defvar easycrypt-proof-weak-mode nil)
@@ -38,7 +45,7 @@
(defun easycrypt-last-prompt-info (s)
"Extract the information from prompt."
- (let ((lastprompt (or s (error "no prompt"))))
+ (let ((lastprompt (or s (error "No prompt"))))
(when (string-match "\\[\\([0-9]+\\)|\\(\\sw+\\)\\]" lastprompt)
(list (string-to-number (match-string 1 lastprompt))
(if (equal (match-string 2 lastprompt) "weakcheck") t nil)))))
@@ -68,3 +75,5 @@
(list (format "undo %s." (int-to-string span-staten)))))
(provide 'easycrypt-hooks)
+
+;;; easycrypt-hooks.el ends here