Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Miscellaneous minimal syntax fixes #56

Open
wants to merge 3 commits into
base: pathogen-bundle
Choose a base branch
from
Open

Miscellaneous minimal syntax fixes #56

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
b2aa621
add Theorem coloration to Fact
dwarfmaster Apr 9, 2017
60f9a28
color all same-typed hypothesis in goal window
dwarfmaster Apr 9, 2017
0f83870
add exfalso to tactic coloring
dwarfmaster Apr 15, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion syntax/coq-goals.vim
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions syntax/coq.vim
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down