(global-set-key [delete] 'delete-char)

(setq load-path 
      (cons (expand-file-name "/usr/local/lib/ProofGeneral-3.3/")
            load-path))

;---------
; mode Coq
;---------

;; Attention il faut Emacs 20.3 !!

(setq load-path 
      (cons (expand-file-name "/usr/local/lib/ProofGeneral-3.3/generic")
            load-path))

(require 'proof-site)

;Raccourcis pour ProofGeneral

(add-hook 'proof-mode-hook '(lambda ()                                 
(define-key proof-mode-map [(control meta down)] 'proof-assert-next-command-interactive)
; commande suivante (lance le process Coq si necessaire)

(define-key proof-mode-map [(control meta up)] 'proof-undo-last-successful-command)
;(define-key proof-mode-map [(control meta up)] 'proof-toolbar-undo)
; undo, revient une commande en arriere

(define-key proof-mode-map [(control meta right)] 'proof-assert-until-point-interactive)
; lire le script jusqu'au curseur (lance le process Coq si necessaire)

(define-key proof-mode-map [(control meta left)] 'proof-retract-until-point-interactive)
; undo jusqu'au curseur

(define-key proof-mode-map [(control meta delete)] 'proof-shell-exit)
; tuer le process Coq, utile car il ne peut y avoir
; qu'un seul process Coq a la fois (1 process par Emacs)

(define-key proof-mode-map [(control meta insert)] 'proof-interrupt-process)
; Pour interrompre le script en cours, le script s'arrete la ou
; il en etait, cette commande peut compromettre la coherence
; avec la partie read-only du buffer (apparemment c'est rare)

(define-key proof-mode-map [(control meta home)] 'proof-retract-buffer)
; reset du script

(define-key proof-mode-map [(control meta end)] 'proof-process-buffer)
; effectuer le script jusqu'a la fin du buffer

(define-key proof-mode-map [(control meta return)] 'proof-minibuffer-cmd)
; pour taper une commande directement, mais sans qu'elle soit ajoutee
; au script

))

(add-hook 'coq-mode-hook 
          '(lambda () 
             (font-lock-fontify-buffer)
             (define-key coq-mode-map "\C-l" 'font-lock-fontify-buffer)
             ))

(custom-set-faces
 '(proof-queue-face        ((((type x) (class color) (background light)) (:background "Thistle"))) t )
 '(proof-locked-face       ((((type x) (class color) (background light)) (:background "LightSteelBlue"))) t)
 '(proof-error-face        ((((type x) (class color) (background light)) (:foreground "steelblue"))) t)
 '(proof-tactics-name-face ((((type x) (class color) (background light)) (:foreground "steelblue"))) t)
 '(proof-declaration-name-face ((((type x) (class color) (background light)) (:foreground "chocolate"))) t)
)

(setq auto-mode-alist (cons '("\\.v" . coq-mode) auto-mode-alist))

(autoload 'coq-mode "proof" "Mode for doing proofs with Proof General")

;; proof general : macro de Pierre pour couper l'Emacs en trois

(defun three-b (b1 b2 b3)
       "Select three existing buffers.
     Put them into three windows, selecting the last one."
         (interactive "bBuffer1:\nbBuffer2:\nbBuffer3:")
         (delete-other-windows)
         (split-window-horizontally)
         (switch-to-buffer b1)
         (split-window-vertically)
         (other-window 1)
         (switch-to-buffer b2)
         (other-window 1)
         (switch-to-buffer b3)
	 (other-window 1))

 (defun coq-three-b ()
   (interactive)
   (three-b (buffer-name (first (buffer-list)))
            "*coq-response*" "*coq-goals*")
 )

(add-hook 'proof-mode-hook 
	  '(lambda ()                                 
 	     (define-key proof-mode-map [f3] 'coq-three-b)))

(global-set-key [f4]   'goto-line)
(global-set-key [f5]   'compile)
(global-set-key [f6]   'recompile)
(global-set-key [f7]   'next-error)
(global-set-key [f12]   'coq-find-file)