From c881047dd32cbd9524b0c733821c113ebcc03b07 Mon Sep 17 00:00:00 2001 From: bn-peters <92739304+bn-peters@users.noreply.github.com> Date: Sat, 30 Mar 2024 22:17:09 +0100 Subject: [PATCH] fix: made edestruct a tactic keyword (#346) --- CHANGELOG.md | 2 ++ syntax/coq.vim | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index ab1627e6..260d532f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,6 +9,8 @@ (PR #339) ### Fixed +- Highlight `edestruct` correctly. + (PR #346) - Highlight `generalize dependent` correctly. (PR #343) - Parse single and double quotes in `_CoqProject` files in the same way as CoqIDE. diff --git a/syntax/coq.vim b/syntax/coq.vim index 7c8070a6..fbaa45dd 100644 --- a/syntax/coq.vim +++ b/syntax/coq.vim @@ -325,7 +325,7 @@ syn keyword coqTactic contained case case_eq casetype cbn cbv change change_n syn keyword coqTactic contained clear clearbody cofix compare compute congr congruence constr_eq constr_eq_nounivs syn keyword coqTactic contained constr_eq_strict constructor contradict contradiction cut cutrewrite cycle syn keyword coqTactic contained decompose destruct dintuition discriminate discrR done dtauto -syn keyword coqTactic contained eapply eassert eassumption easy eauto ecase econstructor eelim eenough eexact eexists +syn keyword coqTactic contained eapply eassert eassumption easy eauto ecase econstructor edestruct eelim eenough eexact eexists syn keyword coqTactic contained einduction einjection eintros eleft elim elimtype enough eremember erewrite eright syn keyword coqTactic contained eset esimplify_eq esplit etransitivity evar exact exact_no_check exactly_once exfalso syn keyword coqTactic contained exists