diff options
| author | Assia Mahboubi | 2015-10-26 18:48:38 +0100 |
|---|---|---|
| committer | Assia Mahboubi | 2015-10-26 18:48:38 +0100 |
| commit | 254379d32d0dac9481b5e54ea54baf613bfd611a (patch) | |
| tree | 695d0bcf0b5ce306f98841695ddadd6e6eab60ba | |
| parent | 00643caee1c2fac0dcc2deb25ec98913c88c224c (diff) | |
Added suport for highlighting gen(erally) have in PG.
| -rw-r--r-- | mathcomp/ssreflect/pg-ssr.el | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/mathcomp/ssreflect/pg-ssr.el b/mathcomp/ssreflect/pg-ssr.el index a2a36fd..a4b845a 100644 --- a/mathcomp/ssreflect/pg-ssr.el +++ b/mathcomp/ssreflect/pg-ssr.el @@ -1,5 +1,5 @@ -;; Customization of PG for ssreflect syntax -;; Assia Mahboubi 2007 +;; Customization of Proof General for highlighting ssreflect tactics. + (defcustom coq-user-tactics-db '(("nat_congr" "ncongr" "nat_congr" t "nat_congr") @@ -9,6 +9,8 @@ ("move" "m" "move" t "move") ("set" "set" "set # := #" t "set") ("have" "hv" "have # : #" t "have") + ("gen have" "genhv" "gen have : / #" t "gen have") + ("generally have" "generhv" "generally have : / #" t "generally have") ("congr" "con" "congr #" t "congr") ("wlog" "wlog" "wlog : / #" t "wlog") ("without loss" "wilog" "without loss #" t "without loss") |