diff options
| author | Pierre Courtieu | 2003-02-04 12:23:03 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2003-02-04 12:23:03 +0000 |
| commit | defde678caf25e8a5110934d0f72d11897135f22 (patch) | |
| tree | f50c4f3b2a49bc83bef66d2d37496cb805b3805b | |
| parent | 141e3000b9cd440b8408948d9ce6bd1b2cda7cab (diff) | |
Coq/pg: fixed a little bug with the "Print Hint" state preserving
command, which must not be matched by the state changing command
"Hint". I put "\\`Hint" in the keyword list, but I am not sure this is
the best way.
| -rw-r--r-- | coq/coq-syntax.el | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 67407b14..006e20d1 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -186,7 +186,7 @@ Print and Check commands, put the following line in your .emacs: "Extraction\\s-+Language" "Extraction\\s-+NoInline" "Grammar" - "Hint" ;; not "Print Hint ." (proof-string-match coq-state-changing-commands-regexp "Hint toto") + "\\`Hint" ;; Pierre fev-2003: Hack: must not match "Print Hint." "Hints" "Identity\\s-+Coercion" "Implicit\\s-+Arguments\\s-+Off" |