fix: made edestruct a tactic keyword (#346)

whonore · Mar 30, 2024 · c881047 · c881047
1 parent 8f24d72
commit c881047
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git 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
@@ -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