diff options
| author |  Assia Mahboubi <assia.mahboubi@inria.fr> | 2007-11-20 16:13:02 +0000 |
|---|---|---|
| committer | Assia Mahboubi <assia.mahboubi@inria.fr> | 2007-11-20 16:13:02 +0000 |
| commit | ad101c11589d26a8b93ecace6aeb7ea447f276d2 (patch) | |
| tree | 85b9eb798eff54adffa5de9208225eaacfa4168c /coq/coq-db.el | |
| parent | 29c75c727b6affd4208c90317e203cf57d4652b4 (diff) | |
adding coq-solve tactics
Diffstat (limited to 'coq/coq-db.el')
| -rw-r--r-- | coq/coq-db.el | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/coq/coq-db.el b/coq/coq-db.el index b29c8c57..5d9e0d65 100644 --- a/coq/coq-db.el +++ b/coq/coq-db.el @@ -207,6 +207,20 @@ See `coq-syntax-db' for DB structure." (nth 3 l)) ; fourth argument is nil --> state preserving command +;;A new face for tactics which fail when they don't kill the current goal +(defface coq-solve-tactics-face + (proof-face-specs + (:foreground "red" t) ; pour les fonds clairs + (:forground "red" t) ; pour les fond foncés + t) ; pour le noir et blanc + "Face for names of closing tactics in proof scripts." + :group 'proof-faces) + +(defconst coq-solve-tactics-face 'coq-solve-tactics-face + "Expression that evaluates to a face. +Required so that 'proof-solve-tactics-face is a proper facename") + + (provide 'coq-db) |