diff options
| author | Pierre Courtieu | 2008-07-21 15:14:58 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2008-07-21 15:14:58 +0000 |
| commit | a4fe36f5e0c3ffc64797bed551176d6d30a04834 (patch) | |
| tree | ef580b8c356619008d0db0bf0f548b2b6181165f | |
| parent | 5b11bdadb77636e56dbfd632c85d443a8e8fe59d (diff) | |
todo added fo coq.
| -rw-r--r-- | coq/TODO-TMP | 10 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 2 | ||||
| -rw-r--r-- | coq/coq.el | 6 | ||||
| -rw-r--r-- | coq/example-utf8.v | 2 |
4 files changed, 15 insertions, 5 deletions
diff --git a/coq/TODO-TMP b/coq/TODO-TMP index 15fb4aa7..23b78c02 100644 --- a/coq/TODO-TMP +++ b/coq/TODO-TMP @@ -1,3 +1,13 @@ + +march 6 2008: +-- line ending with *). are swalloawed when queuing. +-- give a cursor back in goal and response buffer!!! +-- have '_' be a symbol constituent AND compatible with font-lock +-- catch window splitting errors when quitting/relaunching coq +** end march 6 2008 + + + --- multiple file hacking finish --- X-sym wierdness: (1) (warning/warning) Must provide :input-spec --- nick ideas from coq-ide: proof wizard diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index af6aa6b1..27b63888 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -910,7 +910,7 @@ Used by `coq-goal-command-p'" (defvar coq-ids (proof-ids coq-id " ")) (defun coq-first-abstr-regexp (paren end) - (concat paren "\\s-*\\(" coq-ids "\\)\\s-*" end)) + (concat paren "\\s-*\\(" coq-ids "\\)\\s-*" end)) (defcustom coq-variable-highlight-enable t "Activates partial bound variable highlighting" @@ -1,5 +1,5 @@ ;;; coq.el --- Major mode for Coq proof assistant -;; Copyright (C) 1994 - 1998 LFCS Edinburgh. +;; Copyright (C) 1994 - 1998 LFCS Edinburgh. ;; Authors: Healfdene Goguen, Pierre Courtieu ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr> @@ -8,7 +8,7 @@ ;;; Commentary: -;; +;; ;;; History: (require 'proof) @@ -21,7 +21,7 @@ (require 'cl) ; remove-if (require 'span)) -(require 'coq-local-vars) +(require 'coq-local-vars) (require 'coq-syntax) ; determines coq version, sets coq-prog-name ;; ----- coq specific menu is defined in coq-abbrev.el (require 'coq-abbrev) diff --git a/coq/example-utf8.v b/coq/example-utf8.v index 555c7546..4cba17c8 100644 --- a/coq/example-utf8.v +++ b/coq/example-utf8.v @@ -8,7 +8,7 @@ Load "utf8". (* Printing of unicode notation, in *goals* *) -Lemma test : forall A:Prop, A -> A. +Lemma test : ∀ A:Prop, A -> A. auto. Qed. |