From 904d66f4e2dd40f3afb2ba018d953ee5cb379fcc Mon Sep 17 00:00:00 2001 From: Alley Stoughton Date: Tue, 14 Apr 2026 14:52:05 -0400 Subject: [PATCH] Allow EasyCrypt lemma names to begin with `_`. Fix the regular expression `easycrypt-goal-command-regexp` to take out the `nosmt` option (which is no longer EasyCrypt syntax) and allow lemma names to begin with `_`. --- easycrypt/easycrypt-syntax.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/easycrypt/easycrypt-syntax.el b/easycrypt/easycrypt-syntax.el index 48e64a574..4b84d3bd3 100644 --- a/easycrypt/easycrypt-syntax.el +++ b/easycrypt/easycrypt-syntax.el @@ -49,7 +49,7 @@ (defconst easycrypt-goal-command-regexp (concat "^\\(?:local\\s-+\\)?\\(?:" (proof-ids-to-regexp easycrypt-keywords-proof-goal) "\\)" - "\\s-+\\(?:nosmt\\s-+\\)?\\(\\sw+\\)")) + "\\s-+\\([[:word:]_]\\)")) (defun easycrypt-save-command-p (span str) "Decide whether argument is a [save|qed] command or not."