From b2aa62183ff0270cbfd2d6cc04e273438e92602c Mon Sep 17 00:00:00 2001 From: lucas8 Date: Sun, 9 Apr 2017 20:36:40 +0200 Subject: [PATCH 1/3] add Theorem coloration to Fact --- syntax/coq.vim | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/syntax/coq.vim b/syntax/coq.vim index b493ae8..ac779d2 100644 --- a/syntax/coq.vim +++ b/syntax/coq.vim @@ -197,7 +197,7 @@ syn region coqDeclTerm contained contains=@coqTerm matchgroup=coqVernacPunctua syn region coqDeclTerm contained contains=@coqTerm matchgroup=coqVernacPunctuation start=":" end="\.\_s" " Theorems -syn region coqThm contains=coqThmName matchgroup=coqVernacCmd start="\<\%(Program\_s\+\)\?\%(Theorem\|Lemma\|Example\|Corollary\|Remark\)\>" matchgroup=NONE end="\<\%(Qed\|Defined\|Admitted\|Abort\)\.\_s" keepend +syn region coqThm contains=coqThmName matchgroup=coqVernacCmd start="\<\%(Program\_s\+\)\?\%(Theorem\|Lemma\|Example\|Corollary\|Remark\|Fact\)\>" matchgroup=NONE end="\<\%(Qed\|Defined\|Admitted\|Abort\)\.\_s" keepend syn region coqThmName contained contains=coqThmTerm,coqThmBinder matchgroup=coqIdent start="[_[:alpha:]][_'[:alnum:]]*" matchgroup=NONE end="\<\%(Qed\|Defined\|Admitted\|Abort\)\.\_s" syn region coqThmTerm contained contains=@coqTerm,coqProofBody matchgroup=coqVernacCmd start=":" matchgroup=NONE end="\<\%(Qed\|Defined\|Admitted\|Abort\)\>" syn region coqThmBinder contained matchgroup=coqVernacPunctuation start="(" end=")" keepend From 60f9a28093d8f01ba6b986460dedd5fc4c2d5398 Mon Sep 17 00:00:00 2001 From: lucas8 Date: Mon, 10 Apr 2017 00:27:35 +0200 Subject: [PATCH 2/3] color all same-typed hypothesis in goal window --- syntax/coq-goals.vim | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/syntax/coq-goals.vim b/syntax/coq-goals.vim index e5ebdb5..3a902c2 100644 --- a/syntax/coq-goals.vim +++ b/syntax/coq-goals.vim @@ -26,7 +26,7 @@ syn match coqNumberGoals '\d\+ subgoals\?' nextgroup=coqGoal " Hypothesis syn region coqHypothesisBlock contains=coqHypothesis start="^[_[:alpha:]][_'[:alnum:]]*\s*:" end="^$" keepend -syn region coqHypothesis contained contains=coqHypothesisBody matchgroup=coqIdent start="^[_[:alpha:]][_'[:alnum:]]*" matchgroup=NONE end="^\S"me=e-1 +syn region coqHypothesis contained contains=coqHypothesisBody matchgroup=coqIdent start="^\([_[:alpha:]][_'[:alnum:]]*,\s*\)*[_[:alpha:]][_'[:alnum:]]*" matchgroup=NONE end="^\S"me=e-1 syn region coqHypothesisBody contained contains=@coqTerm matchgroup=coqVernacPunctuation start=":" matchgroup=NONE end="^\S"me=e-1 " Separator From 0f8387016a4b5a9b2820f30652c535695999a976 Mon Sep 17 00:00:00 2001 From: lucas8 Date: Sat, 15 Apr 2017 17:34:17 +0200 Subject: [PATCH 3/3] add exfalso to tactic coloring --- syntax/coq.vim | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/syntax/coq.vim b/syntax/coq.vim index ac779d2..6c8838c 100644 --- a/syntax/coq.vim +++ b/syntax/coq.vim @@ -226,7 +226,7 @@ syn region coqProofEnder contained contains=coqIdent matchgroup=coqProofDelim st syn keyword coqTactic contained absurd apply assert assumption auto syn keyword coqTactic contained case[_eq] change clear[body] cofix cbv compare compute congruence constructor contradiction cut[rewrite] syn keyword coqTactic contained decide decompose dependent destruct discriminate double -syn keyword coqTactic contained eapply eassumption econstructor elim[type] equality evar exact eexact exists +syn keyword coqTactic contained eapply eassumption econstructor elim[type] equality evar exact eexact exists exfalso syn keyword coqTactic contained fix f_equal fold functional generalize hnf syn keyword coqTactic contained idtac induction injection instantiate intro[s] intuition inversion[_clear] syn keyword coqTactic contained lapply left move omega pattern pose proof quote