diff options
| -rw-r--r-- | coq/README | 2 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 7 | ||||
| -rw-r--r-- | coq/coq-unicode-tokens.el | 8 | ||||
| -rw-r--r-- | coq/coq.el | 42 | ||||
| -rw-r--r-- | coq/example-tokens.v | 17 | ||||
| -rw-r--r-- | coq/example.v | 5 |
6 files changed, 29 insertions, 52 deletions
@@ -6,7 +6,7 @@ Later contributions by Patrick Loiseleur, Pierre Courtieu, Status: supported Maintainer: Pierre Courtieu -Coq version: 8.0, 8.1 +Coq version: 8.1 Coq homepage: http://coq.inria.fr/ =========================================================================== diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 5cea6f1f..85e9dfd0 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -951,14 +951,15 @@ Used by `coq-goal-command-p'" ;; recognizing global identifiers, see coq-global-p. (defconst coq-save-command-regexp-strict (proof-anchor-regexp - (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save-strict) + (concat "\\(?:Time\\s-+\\)?\\(" (proof-ids-to-regexp coq-keywords-save-strict) "\\)"))) (defconst coq-save-command-regexp (proof-anchor-regexp - (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save) + (concat "\\(?:Time\\s-+\\)?\\(" (proof-ids-to-regexp coq-keywords-save) "\\)"))) + (defconst coq-save-with-hole-regexp - (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save-strict) + (concat "\\(?:Time\\s-+\\)?\\(" (proof-ids-to-regexp coq-keywords-save-strict) "\\)\\s-+\\(" coq-id "\\)\\s-*\\.")) (defconst coq-goal-command-regexp diff --git a/coq/coq-unicode-tokens.el b/coq/coq-unicode-tokens.el index 6d60189b..f89e0928 100644 --- a/coq/coq-unicode-tokens.el +++ b/coq/coq-unicode-tokens.el @@ -122,7 +122,13 @@ ("-|" "⊣") ("\\/" "∨") ("/\\" "∧") - ("~" "¬")) + ("~" "¬") + + ;; A dirty hack for the goals window, shouldn't be input syntax! + ("============================" + "⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯" + bold tactical) + ) ;; an alist of token name, unicode char sequence "Table mapping Coq tokens to Unicode strings. @@ -51,11 +51,8 @@ (defun coq-build-prog-args () (setq coq-prog-args (append (remove-if (lambda (x) (string-match "\\-emacs" x)) coq-prog-args) - (cond - (coq-version-is-V8-0 '("-emacs")) - (t '("-emacs-U"))) - (if coq-translate-to-v8 " -translate"))) - ) + '("-emacs-U") + (if coq-translate-to-v8 " -translate")))) ;; fix it (unless noninteractive ;; compiling @@ -85,15 +82,9 @@ Set to t if you want this feature." (defconst coq-shell-init-cmd (format "Set Undo %s . " coq-default-undo-limit)) -;; da 15/02/03: moved setting of coq-version-is-vX to coq-syntax to -;; fix compilation - (require 'coq-syntax) (require 'coq-indent) -(if coq-version-is-V8-0 - (setq proof-shell-unicode nil)) - (defcustom coq-prog-env nil "*List of environment settings d to pass to Coq process. On Windows you might need something like: @@ -170,11 +161,6 @@ On Windows you might need something like: (defvar coq-shell-outline-heading-end-regexp coq-goal-regexp) -;; all these are to be remove when coq > 8.0 - -(defconst coq-kill-goal-command "Abort. ") -(defconst coq-forget-id-command "Reset %s . ") -(defconst coq-back-n-command "Back %s . ") ;; some of them must kept when v8.1 because they are used by state preserving ;; check when C-c C-v @@ -661,8 +647,6 @@ This is specific to `coq-mode'." (compile (concat "make " (substring n 0 l) ".vo")))) - - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; To guess the command line options ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -697,7 +681,7 @@ This is specific to `coq-mode'." (setq coq-prog-args nil) (concat (substring command 0 (string-match " [^ ]*$" command)) - (if coq-version-is-V8-1 "-emacs-U" "-emacs"))) + "-emacs-U")) coq-prog-name)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -743,10 +727,6 @@ This is specific to `coq-mode'." ;; FIXME da: Does Coq have a help or about command? ;; proof-info-command "Help" - ;; 3.4: this is no longer used: setting to nil - ;; enforces use of find-and-forget always. - (setq proof-kill-goal-command nil) - (setq proof-goal-command-p 'coq-goal-command-p proof-find-and-forget-fn 'coq-find-and-forget pg-topterm-goalhyplit-fn 'coq-goal-hyp @@ -1032,8 +1012,7 @@ This is a value for the `proof-deactivate-scripting-hook'." ((and (proof-try-require 'compile) compile-command (file-exists-p "Makefile")) - ;; NB: compilation is run in the background - ;; in this case! + ;; NB: compilation is run in the background in this case! (let ((compilation-read-command nil)) (call-interactively 'compile))) (coq-compile-file-command @@ -1131,14 +1110,12 @@ Group number 1 matches the name of the library which is required.") ;; Remark: `action' and `string' are known by `proof-shell-insert-hook' (defun coq-preprocessing () ;; NB: dynamic scoping of `string' - (cond - (coq-time-commands - (setq string (concat "Time " string))))) + (if coq-time-commands + (setq string (concat "Time " string)))) (add-hook 'proof-shell-insert-hook 'coq-preprocessing) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; Subterm markup -- it was added to Coq by Healf, but got removed. @@ -1161,16 +1138,11 @@ mouse activation." ;; Context-senstive in-span menu additions ;; -;; da: message to Pierre: I just put these in as examples, -;; maybe you can suggest some better commands to use on -;; `thm'. (Check is maybe not much use since appears before -;; in the buffer anyway) - (defun coq-create-span-menu (span idiom name) (if (string-equal idiom "proof") (let ((thm (span-property span 'name))) (list (vector - "Check" + "Check" ; useful? `(proof-shell-invisible-command ,(format "Check %s." thm))) (vector diff --git a/coq/example-tokens.v b/coq/example-tokens.v index f890eab6..0444162d 100644 --- a/coq/example-tokens.v +++ b/coq/example-tokens.v @@ -10,7 +10,7 @@ Fixpoint toto (x:nat) {struct x} : nat := (* nat should appear as |N *) match x with | O => O (* double arrow here *) - | S y => toto y (* double arrow here *) + | S => toto y (* double arrow here *) end. Lemma titi : forall x:nat,x=x. (* symbolique for-all and nat *) @@ -25,26 +25,27 @@ Fixpoint pow (n m:nat) {struct n} : nat := | S p => m * pow p m end. -Notation " a ,{ b } " := (a - b) +Notation "a,{b}" := (a - b) (at level 1, no associativity). -Notation "a ^^ b" := (pow a b) +Notation "a^^b" := (pow a b) (at level 1, no associativity). -Notation "a ^{ b }" := (pow a b) +Notation "a^{b}" := (pow a b) (at level 1, no associativity). Variable delta:nat. (* greek delta with a sub 1 and the same with super 1 *) -Definition delta__1 := 0. -Definition delta__2 := delta^^1. -Definition delta__3 := delta__2^{delta}. +Definition delta __ 1 := 0. +Definition delta __ 2 := delta^^1. +Definition delta __ 3 := delta__2^{delta}. Parameter a b x:nat. + (* x with a+b subscripted and then superscripted *) -Definition x_a_b':= x^{a+b}. +Definition x_a_b' := x^{a+b}. Definition x_a_b := x,{a+b}. Definition x_a_b'' := x,{a+b}^{a*b}. diff --git a/coq/example.v b/coq/example.v index f482f2ab..939f89c9 100644 --- a/coq/example.v +++ b/coq/example.v @@ -6,7 +6,7 @@ Module Example. -Goal forall (A B:Prop),(A /\ B) -> (B /\ A). +Goal forall (A B:Prop),(A /\ B) -> (B /\ A). intros A B. intros H. elim H. @@ -16,6 +16,3 @@ Goal forall (A B:Prop),(A /\ B) -> (B /\ A). Save and_comms. End Example. - - - |