diff options
| -rw-r--r-- | coq/coq-db.el | 4 | ||||
| -rw-r--r-- | coq/coq-smie-lexer.el | 7 |
2 files changed, 6 insertions, 5 deletions
diff --git a/coq/coq-db.el b/coq/coq-db.el index a0d671ef..3985a588 100644 --- a/coq/coq-db.el +++ b/coq/coq-db.el @@ -254,13 +254,13 @@ See `coq-syntax-db' for DB structure." "Face for names of closing tactics in proof scripts." :group 'proof-faces) -;;A new face for tactics which fail when they don't kill the current goal +;;A new face for cheating tactics (defface coq-cheat-face (proof-face-specs (:background "red") ; pour les fonds clairs (:background "red") ; pour les fond foncés ()) ; pour le noir et blanc - "Face for names of closing tactics in proof scripts." + "Face for names of cheating tactics in proof scripts." :group 'proof-faces) (defconst coq-solve-tactics-face 'coq-solve-tactics-face diff --git a/coq/coq-smie-lexer.el b/coq/coq-smie-lexer.el index c6459206..094a8478 100644 --- a/coq/coq-smie-lexer.el +++ b/coq/coq-smie-lexer.el @@ -514,11 +514,12 @@ The point should be at the beginning of the command name." (coq-smie-search-token-backward '("let" "match" ;"eval" should be "eval in" but this is not supported by search-token-backward "." ) nil - '(("match" . "with") (("let" "eval") . "in"))))) + '(("match" . "with") (("let" ;"eval" + ) . "in"))))) (cond ((member prev-interesting '("." nil)) "in tactic") ((equal prev-interesting "let") "in let") - ((equal prev-interesting "eval in") "in eval") + ;((equal prev-interesting "eval in") "in eval"); not detectable by coq-smie-search-token-backward ((equal prev-interesting "match") "in match") (t "in tactic"))))) @@ -580,7 +581,7 @@ Lemma foo: forall n, (exp "xxx provedby" exp) (exp "as morphism" exp) (exp "with signature" exp) ("match" matchexp "with match" exp "end");expssss - ("let" assigns "in let" exp) ("eval in" assigns "in eval" exp) + ("let" assigns "in let" exp) ;("eval in" assigns "in eval" exp) disabled ("fun" exp "=> fun" exp) ("if" exp "then" exp "else" exp) ("quantif exists" exp ", quantif" exp) ("forall" exp ", quantif" exp) |