From b4ed3cf3ce09c397115e7f75372245724410a187 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 10 Jun 2016 16:57:47 -0400 Subject: Color lia, romega, nia, psatz, nsatz, lra This closes #77 --- coq/coq-syntax.el | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) (limited to 'coq/coq-syntax.el') diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index ef9fb162..66c60582 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -231,17 +231,22 @@ so for the following reasons: ("lazy" "lazy" "lazy beta delta [#] iota zeta" t "lazy") ("lazymatch with" "m" "lazymatch # with\n| # => #\nend") ("left" "left" "left" t "left") + ("lia" nil "lia" t "lia") ("linear" "lin" "linear" t "linear") ("load" "load" "load" t "load") + ("lra" nil "lra" t "lra") ("move after" "mov" "move # after #" t "move") ("multimatch with" "m" "multimatch # with\n| # => #\nend") - ("now_show" nil "now_show" t "now_show") + ("nia" nil "nia" t "nia") + ("now_show" nil "now_show" t "now_show") + ("nsatz" nil "nsatz" t "nsatz") ("omega" "o" "omega" t "omega") ("pattern" "pat" "pattern" t "pattern") ("pattern(s)" "pats" "pattern # , #" t) ("pattern at" "pata" "pattern # at #" t) ("pose" "po" "pose ( # := # )" t "pose") ("prolog" "prol" "prolog" t "prolog") + ("psatz" nil "psatz" t "psatz") ("quote" "quote" "quote" t "quote") ("quote []" "quote2" "quote # [#]" t) ("red" "red" "red" t "red") @@ -260,6 +265,7 @@ so for the following reasons: ("rewrite" "r" "rewrite #" t "rewrite") ("right" "rig" "right" t "right") ;; ("ring" "ring" "ring #" t "ring") + ("romega" nil "romega" t "romega") ("set in * |-" "seth" "set ( # := #) in * |-" t) ("set in *" "set*" "set ( # := #) in *" t) ("set in |- *" "setg" "set ( # := #) in |- *" t) @@ -335,7 +341,13 @@ so for the following reasons: ("fail" "fa" "fail" nil) ("field" "field" "field" t "field") ("gfail" "gfa" "gfail" nil "gfail") + ("lia" nil "lia" t "lia") + ("lra" nil "lra" t "lra") + ("nia" nil "nia" t "nia") + ("nsatz" nil "nsatz" t "nsatz") ("omega" "o" "omega" t "omega") + ("romega" nil "romega" t "romega") + ("psatz" nil "psatz" t "psatz") ("reflexivity" "refl" "reflexivity #" t "reflexivity") ("ring" "ring" "ring #" t "ring") ("solve" nil "solve [ # | # ]" nil "solve") @@ -1184,7 +1196,7 @@ It is used: (defvar coq-id "\\(@\\|_\\|\\w\\)\\(\\w\\|\\s_\\)*") ;; Coq ca start an id with @ or _ (defvar coq-id-shy "\\(?:@\\|_\\|\\w\\)\\(?:\\w\\|\\s_\\)*") -; do not use proof-ids with a space separator! +; do not use proof-ids with a space separator! (defvar coq-ids (concat coq-id "\\(" "\\s-+" coq-id "\\)*")) (defun coq-first-abstr-regexp (paren end) -- cgit v1.2.3