blob: 3ef7271ca02a4c074061d76e7ae8dc2609c7638b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
|
;; Customization of Proof General for highlighting ssreflect tactics.
(defcustom coq-user-tactics-db
'(("nat_congr" "ncongr" "nat_congr" t "nat_congr")
("nat_norm" "nnorm" "nat_norm" t "nat_norm")
("bool_congr" "bcongr" "bool_congr" t "bool_congr")
("prop_congr" "prcongr" "prop_congr" t "prop_congr")
("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")
("unlock" "unlock" "unlock #" t "unlock")
("suffices" "suffices" "suffices # : #" t "suffices")
("suff" "suff" "suff # : #" t "suff")
)
"Extended list of tactics, includings ssr and user defined ones")
(defcustom coq-user-commands-db
'(("Prenex Implicits" "pi" "Prenex Implicits #" t "Prenex\\s-+Implicits")
("Hint View for" "hv" "Hint View for #" t "Hint\\s-+View\\s-+for")
("inside" "ins" nil f "inside")
("outside" "outs" nil f "outside")
("Canonical " nil "Canonical #." t "Canonical")
)
"Extended list of commands, includings ssr and user defined ones")
(defcustom coq-user-tacticals-db
'(("last" "lst" nil t "last"))
"Extended list of tacticals, includings ssr and user defined ones")
(defcustom coq-user-reserved-db
'("is" "isn't" "nosimpl" "of")
"Extended list of keywords, includings ssr and user defined ones")
(defcustom coq-user-solve-tactics-db
'(("done" nil "done" nil "done")
)
"Extended list of closing tactic(al)s, includings ssr and user defined ones")
;; This works only with the cvs version (> 3.7) of Proof General.
(defcustom coq-variable-highlight-enable nil
"Activates partial bound variable highlighting"
)
|
