diff options
| author | Cyril Anaclet | 2020-05-20 16:34:50 +0200 |
|---|---|---|
| committer | Pierre Courtieu | 2020-06-15 16:21:11 +0200 |
| commit | 0f0bb2c00fb7b20fd187cb92d4d2c3f84c4c5987 (patch) | |
| tree | fbc7d9b1462904df9b73b314fc53c08fc2a46450 /coq | |
| parent | 5c3ebac1e8d67f2124d4cbae86134d2a68e2900e (diff) | |
Add coloration for Ltac2 commands
Close #489
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-syntax.el | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 5b8d8c48..d2b48b67 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -493,9 +493,15 @@ so for the following reasons: ("Program Instance" "pinstance" "Program Instance [ # ] => # where \n# := #;\n# := #." t "Program\\s-+Instance") ("Let" "Let" "Let # : # := #." t "Let") ("Local Ltac2" nil "Local Ltac2 # := #." t "Local\\s-+Ltac2") + ("Ltac2 Type" "lt2rty" "Ltac2 Type rec # := #." t "Ltac2 Type rec") ("Ltac2 Type" "lt2ty" "Ltac2 Type # := #." t "Ltac2 Type") ("Ltac2 Type" "lt2oty" "Ltac2 Type # ::= #." t "Ltac2 Type") - ("Ltac2" "lt2" "Ltac2 # := #." t "Ltac2") + ("Ltac2 Type" "lt2wty" "Ltac2 Type #." t "Ltac2 Type") + ("Ltac2" "lt2mr" "Ltac2 mutable rec # := #." t "Ltac2 mutable rec") + ("Ltac2" "lt2m" "Ltac2 mutable # := #." t "Ltac2 mutable") + ("Ltac2" "lt2r" "Ltac2 rec # := #." t "Ltac2 rec") + ("Ltac2" "lt2s" "Ltac2 Set # := #." t "Ltac2 Set") + ("Ltac2" "lt2" "Ltac2 # := #." t "Ltac2") ("Local Ltac" nil "Local Ltac # := #." t "Local\\s-+Ltac") ("Ltac" "ltac" "Ltac # := #." t "Ltac") ("Module :=" "mo" "Module # : # := #." t ) ; careful |