Renamed for new subdirectory structure

3 files changed, 724 insertions, 0 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
new file mode 100644
index 00000000..55d68f35
--- /dev/null
+++ b/coq/coq-syntax.el
@@ -0,0 +1,278 @@
+;; coq-syntax.el Font lock expressions for Coq
+;; Copyright (C) 1997, 1998 LFCS Edinburgh. 
+;; Author: Thomas Kleymann and Healfdene Goguen
+;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk>
+
+;; $Log$
+;; Revision 1.1  1998/09/03 13:51:13  da
+;; Renamed for new subdirectory structure
+;;
+;; Revision 2.0  1998/08/11 14:59:53  da
+;; New branch
+;;
+;; Revision 1.2  1998/08/11 11:43:13  da
+;; Renamed <file>-fontlock to <file>-syntax
+;;
+;; Revision 1.14  1998/06/11 12:20:14  hhg
+;; Added "Scheme" as definition keyword.
+;;
+;; Revision 1.13  1998/06/10 11:38:04  hhg
+;; Added "Mutual Inductive" as definition keyword.
+;; Changed "\\s " into "\\s-" as whitespace pattern.
+;;
+;; Revision 1.12  1998/06/03 18:01:54  hhg
+;; Changed Compute from command to tactic.
+;; Added Fix, Destruct and Cofix as tactics.
+;; Added Local as goal.
+;;
+;; Revision 1.11  1998/06/02 15:33:16  hhg
+;; Minor modifications to comments
+;;
+;; Revision 1.10  1998/05/15 16:13:23  hhg
+;; Added CoFixpoint and tactics.
+;; Changed indentation.
+;;
+;; Revision 1.9  1998/05/05 14:19:39  hhg
+;; Added CoInductive.
+;; Made updates to reflect problem with "Definition", which couldn't be
+;; used with proof scripts.
+;;
+;; Revision 1.8  1998/01/15 13:30:17  hhg
+;; Added coq-shell-cd
+;; Some new fontlocks
+;;
+;; Revision 1.7  1997/11/26 17:12:55  hhg
+;; Incorporated tms's suggestion for simplifying coq-font-lock-keywords-1
+;;
+;; Revision 1.6  1997/11/06 16:46:20  hhg
+;; Updates to Coq fontlock tables
+;;
+;; Revision 1.5  1997/10/30 15:58:29  hhg
+;; Updates for coq, including:
+;; 	* pbp-goal-command and pbp-hyp-command use proof-terminal-string
+;; 	* updates to keywords
+;; 	* fix for goal regexp
+;;
+;; Revision 1.4  1997/10/24 14:51:07  hhg
+;; Changed order of "Inversion_clear" and "Inversion" so that former is
+;; fontified first.
+;; Added "Print" to list of commands.
+;;
+;; Revision 1.3  1997/10/17 14:45:53  hhg
+;; Added "Induction" as tactic
+;;
+;; Revision 1.2  1997/10/13 17:10:29  tms
+;; *** empty log message ***
+;;
+;; Revision 1.1.2.2  1997/10/08 08:22:28  hhg
+;; Updated undo, fixed bugs, more modularization
+;;
+;; Revision 1.1.2.1  1997/10/07 13:34:10  hhg
+;; New structure to share as much as possible between LEGO and Coq.
+;;
+;;
+
+(require 'proof-syntax)
+
+;; ----- keywords for font-lock.
+
+(defvar coq-keywords-decl
+  '(
+"Axiom"
+"Hypothesis"
+"Parameter"
+"Variable"
+))
+
+(defvar coq-keywords-defn
+  '(
+"CoFixpoint"
+"CoInductive"
+"Fixpoint"
+"Inductive"
+"Mutual\\s-+Inductive"
+"Scheme"
+))
+
+(defvar coq-keywords-goal
+  '(
+"Definition"
+"Fact"
+"Goal"
+"Lemma"
+"Local"
+"Remark"
+"Theorem"
+))
+
+(defvar coq-keywords-save
+  '(
+"Defined"
+"Save"
+"Qed"
+))
+
+(defvar coq-keywords-kill-goal '(
+"Abort"
+))
+
+(defvar coq-keywords-commands
+  '(
+"AddPath"
+"Cd"
+"Check"
+"Class"
+"Coercion"
+"DelPath"
+"Eval"
+"Extraction"
+"Focus"
+"Immediate"
+"Hint"
+"Infix"
+"Opaque"
+"Print"
+"Proof"
+"Pwd"
+"Reset"
+"Search"
+"Show"
+"Transparent"
+))
+
+(defvar coq-tactics
+  '(
+"Absurd"
+"Apply"
+"Assumption"
+"Auto"
+"Case"
+"Change"
+"Clear"
+"Cofix"
+"Compute"
+"Constructor"
+"Contradiction"
+"Cut"
+"DHyp"
+"DInd"
+"Dependent"
+"Destruct"
+"Discriminate"
+"Double"
+"EApply"
+"EAuto"
+"Elim"
+"End"
+"Exact"
+"Exists"
+"Fix"
+"Generalize"
+"Grammar"
+"Hnf"
+"Induction"
+"Injection"
+"Intro"
+"Intros"
+"Intuition"
+"Inversion_clear"
+"Inversion"
+"LApply"
+"Left"
+"Linear"
+"Load"
+"Pattern"
+"Program_all"
+"Program"
+"Prolog"
+"Realizer"
+"Red"
+"Reflexivity"
+"Replace"
+"Rewrite"
+"Right"
+"Section"
+"Simplify_eq"
+"Simpl"
+"Specialize"
+"Split"
+"Symmetry"
+"Syntax"
+"Tauto"
+"Transitivity"
+"Trivial"
+"Unfold"
+))
+
+(defvar coq-keywords
+  (append coq-keywords-goal coq-keywords-save coq-keywords-decl
+	  coq-keywords-defn coq-keywords-commands coq-tactics)
+  "All keywords in a Coq script")
+
+(defvar coq-tacticals '(
+"Do"
+"Idtac"
+"OrElse"
+"Repeat"
+"Try"
+))
+
+;; ----- regular expressions
+(defvar coq-error-regexp "^\\(Error\\|Discarding\\|Syntax error\\|System Error\\)"
+  "A regular expression indicating that the Coq process has identified
+  an error.")
+
+(defvar coq-id proof-id)
+
+(defvar coq-ids (proof-ids coq-id))
+
+(defun coq-abstr-regexp (paren char)
+    (concat paren "\\s-*\\(" coq-ids "\\)\\s-*" char))
+
+(defvar coq-font-lock-terms
+  (list
+
+   ;; lambda binders
+   (list (coq-abstr-regexp "\\[" ":") 1 'font-lock-declaration-name-face)
+
+   ;; Pi binders
+   (list (coq-abstr-regexp "(" ":") 1 'font-lock-declaration-name-face)
+   
+   ;; Kinds
+   (cons (concat "\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\s-*\\(("
+		   coq-id ")\\)?") 'font-lock-type-face))
+  "*Font-lock table for Coq terms.")
+
+;; According to Coq, "Definition" is both a declaration and a goal.
+;; It is understood here as being a goal.  This is important for
+;; recognizing global identifiers, see coq-global-p.
+(defconst coq-save-command-regexp
+  (concat "^" (ids-to-regexp coq-keywords-save)))
+(defconst coq-save-with-hole-regexp
+  (concat "\\(" (ids-to-regexp coq-keywords-save)
+	  "\\)\\s-+\\(" coq-id "\\)\\s-*\."))
+(defconst coq-goal-command-regexp
+  (concat "^" (ids-to-regexp coq-keywords-goal)))
+(defconst coq-goal-with-hole-regexp
+  (concat "\\(" (ids-to-regexp coq-keywords-goal)
+	  "\\)\\s-+\\(" coq-id "\\)\\s-*:"))
+(defconst coq-decl-with-hole-regexp
+  (concat "\\(" (ids-to-regexp coq-keywords-decl)
+	  "\\)\\s-+\\(" coq-ids "\\)\\s-*:"))
+(defconst coq-defn-with-hole-regexp
+  (concat "\\(" (ids-to-regexp coq-keywords-defn)
+	  "\\)\\s-+\\(" coq-id "\\)\\s-*[:[]"))
+
+(defvar coq-font-lock-keywords-1
+   (append
+    coq-font-lock-terms
+    (list
+     (cons (ids-to-regexp coq-keywords) 'font-lock-keyword-face)
+     (cons (ids-to-regexp coq-tacticals) 'font-lock-tacticals-name-face)
+
+     (list coq-goal-with-hole-regexp 2 'font-lock-function-name-face)
+     (list coq-decl-with-hole-regexp 2 'font-lock-declaration-name-face)
+     (list coq-defn-with-hole-regexp 2 'font-lock-function-name-face)
+     (list coq-save-with-hole-regexp 2 'font-lock-function-name-face))))
+
+(provide 'coq-syntax)
diff --git a/coq/coq.el b/coq/coq.el
new file mode 100644
index 00000000..3a34ab19
--- /dev/null
+++ b/coq/coq.el
@@ -0,0 +1,390 @@
+;; coq.el Major mode for Coq proof assistant
+;; Copyright (C) 1994 - 1998 LFCS Edinburgh. 
+;; Author: Healfdene Goguen and Thomas Kleymann
+
+;; $Id$
+
+(require 'coq-syntax)
+(require 'outline)
+(require 'proof)
+(require 'info)
+
+; Configuration
+
+(defvar coq-assistant "Coq"
+  "Name of proof assistant")
+
+(defvar coq-tags "/usr/local/lib/coq/theories/TAGS"
+  "the default TAGS table for the Coq library")
+
+(defconst coq-process-config nil
+  "Command to configure pretty printing of the Coq process for emacs.")
+
+(defconst coq-interrupt-regexp "Interrupted"
+  "Regexp corresponding to an interrupt")
+
+(defvar coq-default-undo-limit 100
+  "Maximum number of Undo's possible when doing a proof.")
+
+;; ----- web documentation
+
+(defvar coq-www-home-page "http://pauillac.inria.fr/coq/")
+
+;; ----- coq-shell configuration options
+
+(defvar coq-prog-name "coqtop -emacs"
+  "*Name of program to run as Coq.")
+
+(defvar coq-shell-prompt-pattern (concat "^" proof-id " < ")
+  "*The prompt pattern for the inferior shell running coq.")
+
+(defvar coq-shell-cd nil ; "Cd \"%s\"."
+  "*Command of the inferior process to change the directory.") 
+
+(defvar coq-shell-abort-goal-regexp "Current goal aborted"
+  "*Regular expression indicating that the proof of the current goal
+  has been abandoned.")
+
+(defvar coq-shell-proof-completed-regexp "Subtree proved!"
+  "*Regular expression indicating that the proof has been completed.")
+
+(defvar coq-goal-regexp
+  "\\(============================\\)\\|\\(subgoal [0-9]+ is:\\)\n")
+
+;; ----- outline
+
+(defvar coq-outline-regexp
+  (ids-to-regexp 
+	   '("Section" "Chapter" "Goal" "Lemma" "Theorem" "Fact"
+	   "Remark" "Record" "Inductive" "Definition")))
+
+(defvar coq-outline-heading-end-regexp "\.\\|\\*)")
+
+(defvar coq-shell-outline-regexp coq-goal-regexp)
+(defvar coq-shell-outline-heading-end-regexp coq-goal-regexp)
+
+(defconst coq-kill-goal-command "Abort.")
+(defconst coq-forget-id-command "Reset ")
+
+(defconst coq-undoable-commands-regexp (ids-to-regexp coq-tactics))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;   Derived modes - they're here 'cos they define keymaps 'n stuff ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define-derived-mode coq-shell-mode proof-shell-mode
+   "coq-shell" "Inferior shell mode for coq shell"
+   (coq-shell-mode-config))
+
+(define-derived-mode coq-mode proof-mode
+   "coq" "Coq Mode"
+   (coq-mode-config))
+
+(define-derived-mode coq-pbp-mode pbp-mode
+  "pbp" "Proof-by-pointing support for Coq"
+  (coq-pbp-mode-config))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;   Code that's coq specific                                      ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defun coq-shell-init-hook ()
+  (insert (format "Set Undo %s." coq-default-undo-limit))
+  (insert (format "Cd \"%s\"." default-directory))
+  (remove-hook 'proof-shell-insert-hook 'coq-shell-init-hook))
+
+(defun coq-set-undo-limit (undos)
+  (proof-invisible-command (format "Set Undo %s." undos)))
+
+(defun coq-count-undos (span)
+  (let ((ct 0) str i)
+    (if (and span (prev-span span 'type)
+	     (not (eq (span-property (prev-span span 'type) 'type) 'comment))
+	     (coq-goal-command-p
+	      (span-property (prev-span span 'type) 'cmd)))
+	(concat "Restart" proof-terminal-string)
+      (while span
+	(setq str (span-property span 'cmd))
+	(cond ((eq (span-property span 'type) 'vanilla)
+	       (if (string-match coq-undoable-commands-regexp str)
+		   (setq ct (+ 1 ct))))
+	      ((eq (span-property span 'type) 'pbp)
+	       (cond ((string-match coq-undoable-commands-regexp str)
+		      (setq i 0)
+		      (while (< i (length str))
+			(if (= (aref str i) proof-terminal-char)
+			    (setq ct (+ 1 ct)))
+			(setq i (+ 1 i))))
+		     (t nil))))
+	(setq span (next-span span 'type)))
+      (concat "Undo " (int-to-string ct) proof-terminal-string))))
+
+(defconst coq-keywords-decl-defn-regexp
+  (ids-to-regexp (append coq-keywords-decl coq-keywords-defn))
+  "Declaration and definition regexp.")
+
+(defun coq-goal-command-p (str)
+  "Decide whether argument is a goal or not"
+  (and (string-match coq-goal-command-regexp str)
+       (not (string-match "Definition.*:=" str))))
+
+(defun coq-find-and-forget (span)
+  (let (str ans)
+    (while (and span (not ans))
+      (setq str (span-property span 'cmd))
+      (cond
+
+       ((eq (span-property span 'type) 'comment))       
+
+       ((eq (span-property span 'type) 'goalsave)
+	(setq ans (concat coq-forget-id-command
+			  (span-property span 'name) proof-terminal-string)))
+
+       ((string-match (concat "\\`\\(" coq-keywords-decl-defn-regexp
+                              "\\)\\s-*\\(" proof-id "\\)\\s-*[\\[,:]") str)
+	(setq ans (concat coq-forget-id-command
+			  (match-string 2 str) proof-terminal-string)))
+
+       ;; If it's not a goal but it contains "Definition" then it's a
+       ;; declaration
+       ((and (not (coq-goal-command-p str))
+	     (string-match
+	      (concat "Definition\\s-+\\(" proof-id "\\)\\s-*:") str))
+	(setq ans (concat coq-forget-id-command
+			  (match-string 2 str) proof-terminal-string))))
+
+      (setq span (next-span span 'type)))
+
+      (or ans "COMMENT")))
+
+(defvar coq-current-goal 1
+  "Last goal that emacs looked at.")
+
+(defun coq-goal-hyp ()
+  (cond 
+   ((looking-at "============================\n")
+    (goto-char (match-end 0))
+    (cons 'goal (int-to-string coq-current-goal)))
+   ((looking-at "subgoal \\([0-9]+\\) is:\n")
+    (goto-char (match-end 0))
+    (cons 'goal (match-string 1))
+    (setq coq-current-goal (string-to-int (match-string 1))))
+   ((looking-at proof-shell-assumption-regexp)
+    (cons 'hyp (match-string 1)))
+   (t nil)))
+
+(defun coq-state-preserving-p (cmd)
+  (not (string-match coq-undoable-commands-regexp cmd)))
+
+(defun coq-global-p (cmd)
+  (or (string-match coq-keywords-decl-defn-regexp cmd)
+      (and (string-match
+	    (concat "Definition\\s-+\\(" coq-id "\\)\\s-*:") cmd)
+	   (string-match ":=" cmd))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;   Commands specific to coq                                      ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defun coq-Intros () 
+  "List proof state." 
+  (interactive) 
+  (insert "Intros "))
+
+(defun coq-Apply () 
+  "List proof state."  
+  (interactive) 
+  (insert "Apply "))
+
+(defun coq-Search ()
+  "Search for type in goals."
+  (interactive)
+  (let (cmd)
+    (proof-check-process-available)
+    (setq cmd (read-string "Search Type: " nil 'proof-minibuffer-history))
+    (proof-invisible-command (concat "Search " cmd proof-terminal-string))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;   Indentation                                                    ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; "Case" is represented by 'c' on the stack, and
+;; "CoInductive is represented by 'C'.
+(defun coq-stack-to-indent (stack)
+  (cond
+   ((null stack) 0)
+   ((null (car (car stack)))
+    (nth 1 (car stack)))
+   (t (let ((col (save-excursion
+		   (goto-char (nth 1 (car stack)))
+		   (current-column))))
+	(cond
+	 ((eq (car (car stack)) ?c)
+	  (save-excursion (move-to-column (current-indentation))
+			  (cond 
+			   ((eq (char-after (point)) ?|) (+ col 3))
+			   ((looking-at "end") col)
+			   (t (+ col 5)))))	  
+	 ((or (eq (car (car stack)) ?I) (eq (car (car stack)) ?C))
+	  (+ col (if (eq ?| (save-excursion 
+			      (move-to-column (current-indentation))
+			      (char-after (point)))) 2 4)))
+	 (t (1+ col)))))))
+
+(defun coq-parse-indent (c stack)
+  (cond
+   ((eq c ?C)
+    (cond ((looking-at "Case")
+	   (cons (list ?c (point)) stack))
+	  ((looking-at "CoInductive")
+	   (forward-char (length "CoInductive"))
+	   (cons (list c (- (point) (length "CoInductive"))) stack))
+	  (t stack)))
+   ((and (eq c ?e) (looking-at "end") (eq (car (car stack)) ?c))
+    (cdr stack))
+
+   ((and (eq c ?I) (looking-at "Inductive"))
+    (forward-char (length "Inductive"))
+    (cons (list c (- (point) (length "Inductive"))) stack))
+
+   ((and (eq c ?.) (or (eq (car (car stack)) ?I) (eq (car (car stack)) ?C)))
+    (cdr stack))
+
+   (t stack)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;   Coq shell startup and exit hooks                               ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defun coq-pre-shell-start ()
+  (setq proof-prog-name coq-prog-name)
+  (setq proof-mode-for-shell 'coq-shell-mode)
+  (setq proof-mode-for-pbp 'coq-pbp-mode)
+)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;   Configuring proof and pbp mode and setting up various utilities  ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defun coq-init-syntax-table ()
+  "Set appropriate values for syntax table in current buffer."
+
+  (modify-syntax-entry ?\$ ".")
+  (modify-syntax-entry ?\/ ".")
+  (modify-syntax-entry ?\\ ".")
+  (modify-syntax-entry ?+  ".")
+  (modify-syntax-entry ?-  ".")
+  (modify-syntax-entry ?=  ".")
+  (modify-syntax-entry ?%  ".")
+  (modify-syntax-entry ?<  ".")
+  (modify-syntax-entry ?>  ".")
+  (modify-syntax-entry ?\& ".")
+  (modify-syntax-entry ?_  "_")
+  (modify-syntax-entry ?\' "_")
+  (modify-syntax-entry ?\| ".")
+  (modify-syntax-entry ?\* ". 23")
+  (modify-syntax-entry ?\( "()1")
+  (modify-syntax-entry ?\) ")(4"))
+
+(defun coq-mode-config ()
+
+  (setq proof-terminal-char ?\.)
+  (setq proof-comment-start "(*")
+  (setq proof-comment-end "*)")
+
+  (setq proof-assistant coq-assistant
+	proof-www-home-page coq-www-home-page)
+
+  (setq proof-prf-string "Show"
+	proof-ctxt-string "Print All"
+	proof-help-string "Help")
+
+  (setq proof-goal-command-p 'coq-goal-command-p
+	proof-count-undos-fn 'coq-count-undos
+	proof-find-and-forget-fn 'coq-find-and-forget
+        proof-goal-hyp-fn 'coq-goal-hyp
+	proof-state-preserving-p 'coq-state-preserving-p
+	proof-global-p 'coq-global-p
+	proof-parse-indent 'coq-parse-indent
+	proof-stack-to-indent 'coq-stack-to-indent)
+
+  (setq proof-save-command-regexp coq-save-command-regexp
+	proof-save-with-hole-regexp coq-save-with-hole-regexp
+	proof-goal-with-hole-regexp coq-goal-with-hole-regexp
+	proof-kill-goal-command coq-kill-goal-command
+	proof-commands-regexp (ids-to-regexp coq-keywords))
+
+  (coq-init-syntax-table)
+
+;; font-lock
+
+  (setq font-lock-keywords coq-font-lock-keywords-1)
+
+  (proof-config-done)
+
+  (define-key (current-local-map) [(control c) ?I] 'coq-Intros)
+  (define-key (current-local-map) [(control c) ?a] 'coq-Apply)
+  (define-key (current-local-map) [(control c) (control s)] 'coq-Search)
+
+;; outline
+  
+  (make-local-variable 'outline-regexp)
+  (setq outline-regexp coq-outline-regexp)
+
+  (make-local-variable 'outline-heading-end-regexp)
+  (setq outline-heading-end-regexp coq-outline-heading-end-regexp)
+
+;; tags
+  (and (boundp 'tag-table-alist)
+       (setq tag-table-alist
+	     (append '(("\\.v$" . coq-tags)
+		       ("coq"  . coq-tags))
+		     tag-table-alist)))
+
+  (setq blink-matching-paren-dont-ignore-comments t)
+
+;; hooks and callbacks
+
+  (add-hook 'proof-pre-shell-start-hook 'coq-pre-shell-start nil t))
+
+(defun coq-shell-mode-config ()
+  (setq proof-shell-prompt-pattern coq-shell-prompt-pattern
+        proof-shell-cd coq-shell-cd
+        proof-shell-abort-goal-regexp coq-shell-abort-goal-regexp
+        proof-shell-proof-completed-regexp coq-shell-proof-completed-regexp
+        proof-shell-error-regexp coq-error-regexp
+	proof-shell-interrupt-regexp coq-interrupt-regexp
+        proof-shell-noise-regexp ""
+        proof-shell-assumption-regexp coq-id
+        proof-shell-goal-regexp coq-goal-regexp
+        proof-shell-first-special-char ?\360
+        proof-shell-wakeup-char ?\371 ; done: prompt
+        ; The next three represent path annotation information
+	proof-shell-start-char ?\372 ; not done
+        proof-shell-end-char ?\373 ; not done
+        proof-shell-field-char ?\374 ; not done
+        proof-shell-goal-char ?\375 ; done
+	proof-shell-eager-annotation-start "\376" ; done
+	proof-shell-eager-annotation-end "\377" ; done
+        proof-shell-annotated-prompt-regexp
+	(concat proof-shell-prompt-pattern
+		(char-to-string proof-shell-wakeup-char)) ; done
+        proof-shell-result-start "\372 Pbp result \373"
+        proof-shell-result-end "\372 End Pbp result \373"
+        proof-shell-start-goals-regexp "[0-9]+ subgoals?"
+        proof-shell-end-goals-regexp proof-shell-annotated-prompt-regexp
+        proof-shell-init-cmd nil
+	proof-analyse-using-stack t)
+
+  ;; The following hook is removed once it's called.
+  (add-hook 'proof-shell-insert-hook 'coq-shell-init-hook nil t)
+
+  (coq-init-syntax-table)
+
+  (proof-shell-config-done))
+
+(defun coq-pbp-mode-config ()
+  (setq pbp-change-goal "Show %s.")
+  (setq pbp-error-regexp coq-error-regexp))
+
+(provide 'coq)
diff --git a/coq/coqtags b/coq/coqtags
new file mode 100644
index 00000000..b6c72c78
--- /dev/null
+++ b/coq/coqtags
@@ -0,0 +1,56 @@
+#!/usr/local/bin/perl4
+$/=0777;
+
+if($#ARGV<$[) {die "No Files\n";}
+open(tagfile,">TAGS") || die "Couldn't open TAGS: $!\n";
+
+while(<>)	
+{ 
+  print "Tagging $ARGV\n";
+  $a=$_;
+  $cp=1;
+  $lp=1;
+  $tagstring="";
+
+  while(1) 
+  { 
+
+#   ---- Get the next statement starting on a newline ---- 
+
+    if($a=~/^[ \t\n]*\(\*/)
+    { while($a=~/^\s*\(\*/) 
+      { $d=1; $a=$'; $cp+=length $&; $lp+=($&=~tr/\n/\n/);
+        while($d>0 && $a=~/\(\*|\*\)/)
+        { $a=$'; $cp+=2+length $`; $lp+=($`=~tr/\n/\n/);
+          if($& eq "(*") {$d++} else {$d--};
+        }
+        if($d!=0) {die "Unbalanced Comment?";}
+      }
+    }
+
+    if($cp>1 && $a=~/.*\n/) {$a=$'; $cp+=length $&; $lp++;}
+    while($a=~/^\n/) {$cp++;$lp++;$a=$'}
+
+    if($a=~/^[^\.]*\./) 
+    { $stmt=$&; $newa=$'; $newcp=$cp+length $&; $newlp=$lp+($&=~tr/\n/\n/); }
+    else { last;}
+
+# ---- The above embarrasses itself if there are semicolons inside comments 
+# ---- inside commands. Could do better.
+
+#  print "----- (",$lp,",",$cp,")\n", $stmt, "\n";
+
+    if($stmt=~/^([ \t]*((Fact)|(Goal)|(Lemma)|(Remark)|(Theorem))\s+([\w\']+))\s*:/)
+       { $tagstring.=$1."\177".$8."\001".$lp.",".$cp."\n"; }
+
+    elsif($stmt=~/^([ \t]*((Axiom)|(Hypothesis)|(Parameter)|(Variable))\s+([\w\']+))\s*:/)
+       { $tagstring.=$1."\177".$7."\001".$lp.",".$cp."\n"; }
+
+    elsif($stmt=~/^([ \t]*((Definition)|(Fixpoint)|(Inductive))\s+([\w\']+))\s*[:[]/)
+       { $tagstring.=$1."\177".$6."\001".$lp.",".$cp."\n"; }
+
+    $cp=$newcp; $lp=$newlp; $a=$newa;
+  }  
+  print tagfile "\f\n".$ARGV.",".(length $tagstring)."\n".$tagstring;
+}
+close tagfile;