Merge branch 'master' of github.com:ProofGeneral/PG into master_origin

24 files changed, 1054 insertions, 86 deletions

diff --git a/Makefile b/Makefile
index bcdd1db1..b6006aa0 100644
--- a/Makefile
+++ b/Makefile
@@ -163,14 +163,16 @@ INFODIR=${PREFIX}/share/info
 install: install-desktop install-elisp install-bin install-init
 
 install-desktop:
-	mkdir -p ${DESKTOP}/icons/hicolor/16x16
-	cp etc/desktop/icons/16x16/proofgeneral.png ${DESKTOP}/icons/hicolor/16x16
-	mkdir -p ${DESKTOP}/icons/hicolor/32x32
-	cp etc/desktop/icons/32x32/proofgeneral.png ${DESKTOP}/icons/hicolor/32x32
-	mkdir -p ${DESKTOP}/icons/hicolor/48x48
-	cp etc/desktop/icons/48x48/proofgeneral.png ${DESKTOP}/icons/hicolor/48x48
-	mkdir -p ${DESKTOP}/pixmaps
-	cp etc/desktop/icons/48x48/proofgeneral.png ${DESKTOP}/pixmaps
+	mkdir -p ${DESKTOP}/icons/hicolor/16x16/apps
+	cp etc/desktop/icons/16x16/proofgeneral.png ${DESKTOP}/icons/hicolor/16x16/apps
+	mkdir -p ${DESKTOP}/icons/hicolor/32x32/apps
+	cp etc/desktop/icons/32x32/proofgeneral.png ${DESKTOP}/icons/hicolor/32x32/apps
+	mkdir -p ${DESKTOP}/icons/hicolor/48x48/apps
+	cp etc/desktop/icons/48x48/proofgeneral.png ${DESKTOP}/icons/hicolor/48x48/apps
+	mkdir -p ${DESKTOP}/icons/hicolor/64x64/apps
+	cp etc/desktop/icons/64x64/proofgeneral.png ${DESKTOP}/icons/hicolor/64x64/apps
+	mkdir -p ${DESKTOP}/icons/hicolor/128x128/apps
+	cp etc/desktop/icons/128x128/proofgeneral.png ${DESKTOP}/icons/hicolor/128x128/apps
 	mkdir -p ${DESKTOP}/applications
 	cp etc/desktop/proofgeneral.desktop ${DESKTOP}/applications
 	mkdir -p ${DESKTOP}/mime-info
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 534c013d..2b318dea 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -169,34 +169,68 @@ It was constructed with `proof-defstringset-fn'.")
 		   coq-compile-parallel-in-background)
       :help ,(concat "Continue background compilation after "
 		     "the first error as far as possible")]
-    ["no quick"
-      (customize-set-variable 'coq-compile-quick 'no-quick)
-      :style radio
-      :selected (eq coq-compile-quick 'no-quick)
-      :active (and coq-compile-before-require
-		   coq-compile-parallel-in-background)
-      :help "Compile without -quick but accept existion .vio's"]
-     ["quick no vio2vo"
-      (customize-set-variable 'coq-compile-quick 'quick-no-vio2vo)
-      :style radio
-      :selected (eq coq-compile-quick 'quick-no-vio2vo)
-      :active (and coq-compile-before-require
-		   coq-compile-parallel-in-background)
-      :help "Compile with -quick, accept existing .vo's, don't run vio2vo"]
-     ["quick and vio2vo"
-      (customize-set-variable 'coq-compile-quick 'quick-and-vio2vo)
-      :style radio
-      :selected (eq coq-compile-quick 'quick-and-vio2vo)
-      :active (and coq-compile-before-require
-		   coq-compile-parallel-in-background)
-      :help "Compile with -quick, accept existing .vo's, run vio2vo later"]
-     ["ensure vo"
-      (customize-set-variable 'coq-compile-quick 'ensure-vo)
-      :style radio
-      :selected (eq coq-compile-quick 'ensure-vo)
-      :active (and coq-compile-before-require
-		   coq-compile-parallel-in-background)
-      :help "Ensure only vo's are used for consistency"]
+     ("Quick compilation"
+      ["no quick"
+       (customize-set-variable 'coq-compile-quick 'no-quick)
+       :style radio
+       :selected (eq coq-compile-quick 'no-quick)
+       :active (and coq-compile-before-require
+		    coq-compile-parallel-in-background)
+       :help "Compile without -quick but accept existion .vio's"]
+      ["quick no vio2vo"
+       (customize-set-variable 'coq-compile-quick 'quick-no-vio2vo)
+       :style radio
+       :selected (eq coq-compile-quick 'quick-no-vio2vo)
+       :active (and coq-compile-before-require
+		    coq-compile-parallel-in-background)
+       :help "Compile with -quick, accept existing .vo's, don't run vio2vo"]
+      ["quick and vio2vo"
+       (customize-set-variable 'coq-compile-quick 'quick-and-vio2vo)
+       :style radio
+       :selected (eq coq-compile-quick 'quick-and-vio2vo)
+       :active (and coq-compile-before-require
+		    coq-compile-parallel-in-background)
+       :help "Compile with -quick, accept existing .vo's, run vio2vo later"]
+      ["ensure vo"
+       (customize-set-variable 'coq-compile-quick 'ensure-vo)
+       :style radio
+       :selected (eq coq-compile-quick 'ensure-vo)
+       :active (and coq-compile-before-require
+		    coq-compile-parallel-in-background)
+       :help "Ensure only vo's are used for consistency"]
+      )
+     ("Auto Save"
+      ["Query coq buffers"
+       (customize-set-variable 'coq-compile-auto-save 'ask-coq)
+       :style radio
+       :selected (eq coq-compile-auto-save 'ask-coq)
+       :active coq-compile-before-require
+       :help "Ask for each coq-mode buffer, except the current buffer"]
+      ["Query all buffers"
+       (customize-set-variable 'coq-compile-auto-save 'ask-all)
+       :style radio
+       :selected (eq coq-compile-auto-save 'ask-all)
+       :active coq-compile-before-require
+       :help "Ask for all buffers"]
+      ["Autosave coq buffers"
+       (customize-set-variable 'coq-compile-auto-save 'save-coq)
+       :style radio
+       :selected (eq coq-compile-auto-save 'save-coq)
+       :active coq-compile-before-require
+       :help "Save all Coq buffers without confirmation, except the current one"]
+      ["Autosave all buffers"
+       (customize-set-variable 'coq-compile-auto-save 'save-all)
+       :style radio
+       :selected (eq coq-compile-auto-save 'save-all)
+       :active coq-compile-before-require
+       :help "Save all buffers without confirmation"]
+      )
+     ["Lock Ancesotors"
+      coq-lock-ancestors-toggle
+      :style toggle
+      :selected coq-lock-ancestors
+      :active coq-compile-before-require
+      :help "Lock files of imported modules"]
      ["Confirm External Compilation"
       coq-confirm-external-compilation-toggle
       :style toggle
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index af3e70a4..72a16881 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -42,9 +42,9 @@ Must be used together with `coq-seq-disable'."
   (add-hook 'proof-shell-extend-queue-hook
 	    'coq-par-preprocess-require-commands)
   (add-hook 'proof-shell-signal-interrupt-hook
-	    'coq-par-emergency-cleanup)
+	    'coq-par-user-interrupt)
   (add-hook 'proof-shell-handle-error-or-interrupt-hook
-	    'coq-par-emergency-cleanup))
+	    'coq-par-user-interrupt))
 
 (defun coq-par-disable ()
   "Disable parallel compilation.
@@ -52,9 +52,9 @@ Must be used together with `coq-seq-enable'."
   (remove-hook 'proof-shell-extend-queue-hook
 	       'coq-par-preprocess-require-commands)
   (remove-hook 'proof-shell-signal-interrupt-hook
-	       'coq-par-emergency-cleanup)
+	       'coq-par-user-interrupt)
   (remove-hook 'proof-shell-handle-error-or-interrupt-hook
-	       'coq-par-emergency-cleanup))
+	       'coq-par-user-interrupt))
 
 (defun coq-seq-enable ()
   "Enable sequential synchronous compilation.
@@ -246,7 +246,10 @@ quick-and-vio2vo Same as `quick-no-vio2vo', but start vio2vo processes
 ensure-vo        Ensure that all library dependencies are present as .vo
                  files and delete outdated .vio files or .vio files that
                  are more recent than the corresponding .vo file. This
-                 setting is the only one that ensures soundness."
+                 setting is the only one that ensures soundness.
+
+This option can be set via menu
+`Coq -> Auto Compilation -> Quick compilation'."
   :type
   '(radio
     (const :tag "don't use -quick but accept existing vio files" no-quick)
@@ -371,7 +374,10 @@ This makes four permitted values: 'ask-coq to confirm saving all
 modified Coq buffers, 'ask-all to confirm saving all modified
 buffers, 'save-coq to save all modified Coq buffers without
 confirmation and 'save-all to save all modified buffers without
-confirmation."
+confirmation.
+
+This option can be set via menu
+`Coq -> Auto Compilation -> Auto Save'."
   :type
   '(radio
     (const :tag "ask for each coq-mode buffer, except the current buffer"
@@ -389,17 +395,24 @@ confirmation."
   "If non-nil, lock ancestor module files.
 If external compilation is used (via `coq-compile-command') then
 only the direct ancestors are locked. Otherwise all ancestors are
-locked when the \"Require\" command is processed."
+locked when the \"Require\" command is processed.
+
+This option can be set via menu
+`Coq -> Auto Compilation -> Lock Ancestors'."
+
   :type 'boolean
   :safe 'booleanp
   :group 'coq-auto-compile)
 
+;; define coq-lock-ancestors-toggle
+(proof-deftoggle coq-lock-ancestors)
+
 (defpacustom confirm-external-compilation t
   "If set let user change and confirm the compilation command.
 Otherwise start the external compilation without confirmation.
 
 This option can be set/reset via menu
-`Coq -> Settings -> Confirm External Compilation'."
+`Coq -> Auto Compilation -> Confirm External Compilation'."
   :type 'boolean
   :group 'coq-auto-compile)
 
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index 8901a008..f9b317c2 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -756,20 +756,15 @@ Used for unlocking ancestors on compilation errors."
 	 (put job 'lock-state 'unlocked)))
      coq--compilation-object-hash)))
 
-(defun coq-par-emergency-cleanup ()
-  "Emergency cleanup for parallel background compilation.
-Kills all processes, unlocks ancestors, clears the queue region
-and resets the internal state."
-  (interactive)				; needed for menu
-  (let (proc-killed was-busy)
+(defun coq-par-kill-and-cleanup ()
+  "Kill all background compilation, cleanup internal state and unlock ancestors.
+This is the common core of `coq-par-emergency-cleanup' and
+`coq-par-user-interrupt'. Returns t if there actually was a
+background job that was killed."
+  (let (proc-killed)
     (when coq--debug-auto-compilation
-      (message "emergency cleanup"))
+      (message "kill all jobs and cleanup state"))
     (setq proc-killed (coq-par-kill-all-processes))
-    (when (and (boundp 'prover-was-busy)
-	       (or proc-killed coq--last-compilation-job
-		   coq--compile-vio2vo-in-progress
-		   coq--compile-vio2vo-delay-timer))
-      (setq prover-was-busy t))
     (setq coq-par-compilation-queue (coq-par-new-queue))
     (setq coq--last-compilation-job nil)
     (setq coq-par-vio2vo-queue (coq-par-new-queue))
@@ -778,12 +773,62 @@ and resets the internal state."
       (cancel-timer coq--compile-vio2vo-delay-timer)
       (setq coq--compile-vio2vo-delay-timer nil))
     (coq-par-unlock-all-ancestors-on-error)
-    (when proof-action-list
-      (setq proof-shell-interrupt-pending t))
-    (proof-release-lock)
-    (proof-detach-queue)
     (setq proof-second-action-list-active nil)
-    (coq-par-init-compilation-hash)))
+    (coq-par-init-compilation-hash)
+    proc-killed))
+
+(defun coq-par-emergency-cleanup ()
+  "Emergency cleanup for errors in parallel background compilation.
+This is the function that cleans everything up when some
+background compilation process detected a severe error. When
+`coq-compile-keep-going' is nil, all errors are severe. When
+`coq-compile-keep-going' is t, coqc and some coqdep errors are
+not severe. This function is also used for the user action to
+kill all background compilation.
+
+On top of `coq-par-kill-and-cleanup', this function resets the
+queue region (and thus `proof-action-list' and signals an
+interrupt to the proof shell."
+  (interactive)				; needed for menu
+  (when coq--debug-auto-compilation
+    (message "emergency cleanup"))
+  (coq-par-kill-and-cleanup)
+  (when proof-action-list
+    (setq proof-shell-interrupt-pending t))
+  (proof-release-lock)
+  (proof-detach-queue))
+
+(defun coq-par-user-interrupt ()
+  "React to a generic user interrupt with cleaning up everything.
+This function cleans up background compilation when the proof
+assistant died (`proof-shell-handle-error-or-interrupt-hook') or
+when the user interrupted Proof General (with C-c C-c or
+`proof-interrupt-process' leading to
+`proof-shell-signal-interrupt-hook').
+
+On top of `coq-par-kill-and-cleanup', this function only sets the
+dynamic variable `prover-was-busy' to tell the proof shell that
+the user actually had a reason to interrupt. However, in the
+special case where `proof-action-list' is nil and
+`coq--last-compilation-job' not, this function also clears the
+queue region and releases the proof shell lock. This has the nice
+side effect, that `proof-interrupt-process' does not send an
+interrupt signal to the prover."
+  (let (proc-killed
+	(was-busy (or coq--last-compilation-job
+		      coq--compile-vio2vo-in-progress
+		      coq--compile-vio2vo-delay-timer)))
+    (when coq--debug-auto-compilation
+      (message "cleanup on user interrupt"))
+    (setq proc-killed (coq-par-kill-and-cleanup))
+    (unless proof-action-list
+      (when coq--debug-auto-compilation
+	(message "clear queue region and proof shell lock"))
+      (proof-release-lock)
+      (proof-detach-queue))
+    (when (and (boundp 'prover-was-busy)
+	       (or proc-killed was-busy))
+      (setq prover-was-busy t))))
 
 (defun coq-par-process-filter (process output)
   "Store output from coq background compilation."
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 5aa41292..5844be74 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -411,7 +411,9 @@ so for the following reasons:
 (defvar coq-decl-db
   '(
     ("Local Axiom" nil "Local Axiom # : #" t "Local\\s-+Axiom")
+    ("Local Axioms" nil "Local Axioms # , #: #" t "Local\\s-+Axioms")
     ("Axiom" "ax" "Axiom # : #" t "Axiom")
+    ("Axioms" "axs" "Axioms # , #: #" t "Axioms")
     ("Global Variable" "gv" "Global Variable #: #." t "Global\\s-+Variable")
     ("Global Variables" "gvs" "Global Variables # , #: #." t "Global\\s-+Variables")
     ("Hint Constructors" "hc" "Hint Constructors # : #." t "Hint\\s-+Constructors")
@@ -427,10 +429,11 @@ so for the following reasons:
     ("Hypothesis" "hyp" "Hypothesis #: #" t "Hypothesis")
     ("Hypotheses" "hyp" "Hypotheses #: #" t "Hypotheses")
     ("Parameter" "par" "Parameter #: #" t "Parameter")
-    ("Parameters" "par" "Parameter #: #" t "Parameters")
+    ("Parameters" "par" "Parameters #: #" t "Parameters")
     ("Conjecture" "conj" "Conjecture #: #." t "Conjecture")
     ("Variable" "v" "Variable #: #." t "Variable")
     ("Variables" "vs" "Variables # , #: #." t "Variables")
+    ("Context" nil "Context #, (# : #)." t "Context")
     ("Local Coercion" nil "Local Coercion @{id} : @{typ1} >-> @{typ2}." t "Local\\s-+Coercion")
     ("Coercion" "coerc" "Coercion @{id} : @{typ1} >-> @{typ2}." t "Coercion")
     )
diff --git a/coq/coq-system.el b/coq/coq-system.el
index 88ce06be..0b9b6c58 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -170,6 +170,18 @@ Returns nil if the version can't be detected."
 	 (signal 'coq-unclassifiable-version  coq-version-to-use))
 	(t (signal (car err) (cdr err))))))))
 
+(defun coq--post-v86 ()
+  "Return t if the auto-detected version of Coq is >= 8.6.
+Return nil if the version cannot be detected."
+  (let ((coq-version-to-use (or (coq-version t) "8.5")))
+    (condition-case err
+	(not (coq--version< coq-version-to-use "8.6"))
+      (error
+       (cond
+	((equal (substring (cadr err) 0 15) "Invalid version")
+	 (signal 'coq-unclassifiable-version  coq-version-to-use))
+	(t (signal (car err) (cdr err))))))))
+
 (defcustom coq-use-makefile nil
   "Whether to look for a Makefile to attempt to guess the command line.
 Set to t if you want this feature, but note that it is deprecated."
diff --git a/coq/coq.el b/coq/coq.el
index e3541b48..f6c67475 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -24,6 +24,8 @@
   (defvar proof-info nil)       ; dynamic scope in proof-tree-urgent-action
   (defvar action nil)       ; dynamic scope in coq-insert-as stuff
   (defvar string nil)       ; dynamic scope in coq-insert-as stuff
+  (defvar old-proof-marker nil)
+                         ; dynamic scoq in coq-proof-tree-enable-evar-callback
   (defvar coq-auto-insert-as nil)    ; defpacustom
   (defvar coq-time-commands nil)        ; defpacustom
   (defvar coq-use-project-file t)        ; defpacustom
@@ -1542,6 +1544,12 @@ Near here means PT is either inside or just aside of a comment."
 ;; FIXME da: Does Coq have a help or about command?
 ;;	proof-info-command "Help"
 
+  ;; Settings not defined with defpacustom because they have an unsupported
+  ;; type.
+  (setq proof-assistant-additional-settings
+        '(coq-compile-quick coq-compile-keep-going
+          coq-compile-auto-save coq-lock-ancestors))
+
   (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
@@ -1851,14 +1859,19 @@ not finished, because Coq 8.5 lists open existential variables
 as (new) open subgoals. For this test we assume that
 `proof-marker' has not yet been moved.
 
+The `proof-tree-urgent-action-hook' is also called for undo
+commands. For those, nothing is done.
+
 The not yet delayed output is in the region
 \[proof-shell-delayed-output-start, proof-shell-delayed-output-end]."
   ;; (message "CPTGNS start %s end %s"
   ;;          proof-shell-delayed-output-start
   ;;          proof-shell-delayed-output-end)
-  (with-current-buffer proof-shell-buffer
-    (let ((start proof-shell-delayed-output-start)
-          (end proof-shell-delayed-output-end))
+  (let ((start proof-shell-delayed-output-start)
+        (end proof-shell-delayed-output-end)
+        (state  (car proof-info)))
+  (when (> state proof-tree-last-state)
+    (with-current-buffer proof-shell-buffer
       ;; The message "All the remaining goals are on the shelf" is processed as
       ;; urgent message and is therefore before
       ;; proof-shell-delayed-output-start. We therefore need to go back to
@@ -1879,7 +1892,7 @@ The not yet delayed output is in the region
                            '(no-goals-display
                              no-response-display
                              proof-tree-show-subgoal))
-                          proof-action-list)))))))))
+                          proof-action-list))))))))))
   
 (add-hook 'proof-tree-urgent-action-hook 'coq-proof-tree-get-new-subgoals)
 
@@ -1916,6 +1929,103 @@ This is the Coq incarnation of `proof-tree-find-undo-position'."
     (span-start span-res)))
 
 
+;; In Coq 8.6 the evar line is disabled by default because on some proofs it
+;; causes a severe performance hit. The disabled evar line causes prooftree to
+;; crash with a parsing error. Proof General must therefore turn on the evar
+;; output with the command "Set Printing Dependent Evars Line". Of course,
+;; after the proof, the evar line must be set back to what it was before the
+;; proof. I therefore look in the urgent action hook if proof display is
+;; switched on or off. When switched on, I test the current evar printing
+;; status with the undodumented command "Test Printing Dependent Evars Line" to
+;; remember if I have to switch evar printing off eventually.
+
+(defvar coq--proof-tree-must-disable-evars nil
+  "Remember if evar printing must be disabled when leaving the current proof.")
+
+(defun coq-proof-tree-enable-evar-callback (span)
+  "Callback for the evar printing status test.
+This is the callback for the command ``Test Printing Dependent
+Evars Line''. It checks whether evar printing was off and
+remembers that fact in `coq--proof-tree-must-disable-evars'."
+  (with-current-buffer proof-shell-buffer
+    (save-excursion
+      ;; When the callback runs, the next item is sent to Coq already and
+      ;; therefore proof-marker points to the end of the next command
+      ;; already. proof-shell-filter-manage-output sets old-proof-marker
+      ;; before calling proof-shell-exec-loop, this therefore points to the
+      ;; end of the command of this callback.
+      (goto-char old-proof-marker)
+      (when (re-search-forward "The Printing Dependent Evars Line mode is "
+                               nil t)
+        (if (looking-at "off")
+            (progn
+              ;; (message "CPTEEC evar line mode was off")
+              (setq coq--proof-tree-must-disable-evars t))
+          ;; (message "CPTEEC evar line mode was on")
+          (setq coq--proof-tree-must-disable-evars nil))))))
+
+(defun coq-proof-tree-insert-evar-command (cmd &optional callback)
+  "Insert an evar printing command at the head of `proof-action-list'."
+  (push (proof-shell-action-list-item
+         (concat cmd " Printing Dependent Evars Line.")
+         (if callback callback 'proof-done-invisible)
+         (list 'invisible))
+        proof-action-list))
+
+(defun coq-proof-tree-enable-evars ()
+  "Enable the evar status line for Coq >= 8.6.
+Test the status of evar printing to be able to set it back
+properly after the proof and enable the evar printing."
+  (when (coq--post-v86)
+    ;; We push to proof-action-list --- therefore we need to push in reverse
+    ;; order!
+    (coq-proof-tree-insert-evar-command "Set")
+    (coq-proof-tree-insert-evar-command
+     "Test"
+     'coq-proof-tree-enable-evar-callback)))
+
+(defun coq-proof-tree-disable-evars ()
+  "Disable evar printing if necessary.
+This function switches off evar printing after the proof, if it
+was off before the proof. For undo commands, we rely on the fact
+that Coq itself undos the effect of the evar printing change that
+we inserted after the goal statement. We also rely on the fact
+that Proof General never backtracks into the middle of a
+proof. (If this would happen, Coq would switch evar printing on
+and the code here would not switch it off after the proof.)
+
+Being called from `proof-tree-urgent-action-hook', this function
+can rely on `proof-info' being dynamically bound to the last
+result of `coq-proof-tree-get-proof-info'."
+  (when coq--proof-tree-must-disable-evars
+    (when (> (car proof-info) proof-tree-last-state)
+      (coq-proof-tree-insert-evar-command "Unset"))
+    (setq coq--proof-tree-must-disable-evars nil)))
+
+(defun coq-proof-tree-evar-display-toggle ()
+  "Urgent action hook function for changing the evar printing status in Coq.
+This function is for `proof-tree-urgent-action-hook' (which is
+called only if external proof disaply is switched on). It checks
+whether a proof was started or stopped and inserts commands for
+enableing and disabling the evar status line for Coq 8.6 or
+later. Without the evar status line being enabled, prooftree
+crashes.
+
+Must only be called via `proof-tree-urgent-action-hook' to ensure
+that the dynamic variable `proof-info' is bound to the current
+result of `coq-proof-tree-get-proof-info'."
+  (let ((current-proof-name (cadr proof-info)))
+    (cond
+     ((and (null proof-tree-current-proof) current-proof-name)
+      ;; started a new proof
+      (coq-proof-tree-enable-evars))
+     ((and proof-tree-current-proof (null current-proof-name))
+      ;; finished the current proof
+      (coq-proof-tree-disable-evars)))))
+
+(add-hook 'proof-tree-urgent-action-hook 'coq-proof-tree-evar-display-toggle)
+
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Pre-processing of input string
diff --git a/coq/coqtags b/coq/coqtags
index 6d874e9d..76b5bcc9 100755
--- a/coq/coqtags
+++ b/coq/coqtags
@@ -52,7 +52,7 @@ while(<>)
        { $tagstring.=$1."\177".$8."\001".$lp.",".$cp."\n"; }
 
     elsif($stmt=~/^([ \t]*((Axiom)|(Hypothesis)|(Parameter)|(Variable))\s+[\w\']+)/)
-      { do adddecs($stmt,$1) }
+      { adddecs($stmt,$1); }
 
     elsif($stmt=~/^([ \t]*((Definition)|(Fixpoint)|(Inductive))\s+[\w\']+)/)
        { $tagstring.=$1."\177".$6."\001".$lp.",".$cp."\n"; }
diff --git a/doc/Makefile.doc b/doc/Makefile.doc
index b5eb4d82..b2e69d53 100644
--- a/doc/Makefile.doc
+++ b/doc/Makefile.doc
@@ -18,7 +18,7 @@
 
 MAKE = make -f Makefile.doc 
 MAKEINFO = makeinfo
-TEXI2HTML = texi2html -expandinfo -number-sections -split_chapter --noheader --css-include proofgen.css
+TEXI2HTML = makeinfo --html --ifinfo --number-sections --split=chapter --no-headers --css-include=proofgen.css
 # `texinfo-tex' package contains texi2pdf
 TEXI2PDF = texi2pdf
 # `dviutils' package contains these useful utilities.
@@ -50,7 +50,7 @@ default: doc
 	$(TEXI2PDF) $< 
 
 .texi.html:	
-	$(TEXI2HTML) --output $* $< 
+	$(TEXI2HTML) $<
 
 default: doc
 
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index cf88d683..44c40549 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -361,7 +361,7 @@ file for the mode, which will be
 where @var{proof-home-directory} is the value of the
 variable @samp{@code{proof-home-directory}}.
 
-The default value is @code{((isar "Isabelle" "thy") (coq "Coq" "v" nil (".vo" ".glob")) (phox "PhoX" "phx") (pgshell "PG-Shell" "pgsh") (pgocaml "PG-OCaml" "pgml") (pghaskell "PG-Haskell" "pghci"))}.
+The default value is @code{((isar "Isabelle" "thy") (coq "Coq" "v" nil (".vo" ".glob")) (easycrypt "EasyCrypt" "ec" ".*\\.eca?") (pgshell "PG-Shell" "pgsh") (pgocaml "PG-OCaml" "pgml") (pghaskell "PG-Haskell" "pghci"))}.
 @end defopt
 
 
@@ -3258,7 +3258,7 @@ in the @code{proof-assistants} setting.
 @c TEXI DOCSTRING MAGIC: proof-assistants
 @defopt proof-assistants 
 Choice of proof assistants to use with Proof General.@*
-A list of symbols chosen from: @code{'isar} @code{'coq} @code{'phox} @code{'pgshell} @code{'pgocaml} @code{'pghaskell}.
+A list of symbols chosen from: @code{'isar} @code{'coq} @code{'easycrypt} @code{'pgshell} @code{'pgocaml} @code{'pghaskell}.
 If nil, the default will be ALL available proof assistants.
 
 Each proof assistant defines its own instance of Proof General,
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 442ce6d5..8dab17f0 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -4667,8 +4667,9 @@ ancestor.
 You have two choices, if you don't like ancestor locking in its
 default way.
 You can either switch ancestor locking completely off via
+menu @code{Coq -> Auto Compilation -> Lock Ancestors} or
 @code{coq-lock-ancestors} (@ref{Customizing Coq Multiple
-File Support}) or you can generally permit editing in locked
+File Support}). Alternatively, you can generally permit editing in locked
 sections with selecting 
 @code{Proof-General} -> @code{Quick Options} -> @code{Read Only}
 -> @code{Freely Edit} (which will set the option
@@ -4689,7 +4690,8 @@ file.]
 Proof General supports quick compilation only with the parallel
 asynchronous compilation. There are 4 modes that can be
 configured with @code{coq-compile-quick} or by selecting one of
-the radio buttons in the @code{Coq -> Auto Compilation} menu.
+the radio buttons in the @code{Coq -> Auto Compilation -> Quick
+compilation} menu.
 
 Use the default @code{no-quick}, if you have not yet switched to
 @code{Proof using}. Use @code{quick-no-vio2vo}, if you want quick
@@ -4824,6 +4826,9 @@ modified Coq buffers, @code{'ask-all} to confirm saving all modified
 buffers, @code{'save-coq} to save all modified Coq buffers without
 confirmation and @code{'save-all} to save all modified buffers without
 confirmation.
+
+This option can be set via menu
+@samp{Coq -> Auto Compilation -> Auto Save}.
 @end defvar
 
 
@@ -4899,6 +4904,9 @@ If non-nil, lock ancestor module files.@*
 If external compilation is used (via @samp{@code{coq-compile-command}}) then
 only the direct ancestors are locked. Otherwise all ancestors are
 locked when the "Require" command is processed.
+
+This option can be set via menu
+@samp{Coq -> Auto Compilation -> Lock Ancestors}.
 @end defvar
 
 
@@ -4942,7 +4950,7 @@ If set let user change and confirm the compilation command.@*
 Otherwise start the external compilation without confirmation.
 
 This option can be set/reset via menu
-@samp{Coq -> Settings -> Confirm External Compilation}.
+@samp{Coq -> Auto Compilation -> Confirm External Compilation}.
 @end defvar
 
 
diff --git a/easycrypt/easycrypt-abbrev.el b/easycrypt/easycrypt-abbrev.el
new file mode 100644
index 00000000..3850ffb7
--- /dev/null
+++ b/easycrypt/easycrypt-abbrev.el
@@ -0,0 +1,25 @@
+;; --------------------------------------------------------------------
+;; Copyright (c) - 2012--2016 - IMDEA Software Institute
+;; Copyright (c) - 2012--2016 - Inria
+;;
+;; Distributed under the terms of the GPL-v3 license
+;; --------------------------------------------------------------------
+
+(require 'proof)
+(require 'easycrypt-syntax)
+
+(defpgdefault menu-entries
+  '(
+    ["Use Three Panes" proof-three-window-toggle
+      :style    toggle
+      :active   (not proof-multiple-frames-enable)
+      :selected proof-three-window-enable
+      :help     "Use three panes"]
+
+    ["Weak-check mode" easycrypt-proof-weak-mode-toggle
+     :style    toggle
+     :selected easycrypt-proof-weak-mode
+     :help     "Toggles EasyCrypt check mode."]
+))
+
+(provide 'easycrypt-abbrev)
diff --git a/easycrypt/easycrypt-hooks.el b/easycrypt/easycrypt-hooks.el
new file mode 100644
index 00000000..3cf891e3
--- /dev/null
+++ b/easycrypt/easycrypt-hooks.el
@@ -0,0 +1,70 @@
+;; --------------------------------------------------------------------
+;; Copyright (c) - 2012--2016 - IMDEA Software Institute
+;; Copyright (c) - 2012--2016 - Inria
+;;
+;; Distributed under the terms of the GPL-v3 license
+;; --------------------------------------------------------------------
+
+(require 'span)
+(require 'proof)
+
+(defvar easycrypt-last-but-one-statenum 0)
+(defvar easycrypt-proof-weak-mode nil)
+
+;; Proof mode
+(defun easycrypt-proof-weak-mode-toggle ()
+  "Toggle EasyCrypt check mode."
+  (interactive)
+  (cond
+     (easycrypt-proof-weak-mode
+        (proof-shell-invisible-cmd-get-result "pragma Proofs:check"))
+     (t (proof-shell-invisible-cmd-get-result "pragma Proofs:weak")))
+  (if
+      (eq 'error proof-shell-last-output-kind)
+      (message "Failed to set proof mode")))
+
+;; Function for set or get the information in the span
+(defsubst easycrypt-get-span-statenum (span)
+  "Return the state number of the SPAN."
+  (span-property span 'statenum))
+
+(defsubst easycrypt-set-span-statenum (span val)
+  "Set the state number of the SPAN to VAL."
+  (span-set-property span 'statenum val))
+
+(defsubst proof-last-locked-span ()
+  (with-current-buffer proof-script-buffer
+  (span-at (- (proof-unprocessed-begin) 1) 'type)))
+
+(defun easycrypt-last-prompt-info (s)
+  "Extract the information from prompt."
+  (let ((lastprompt (or s (error "no prompt"))))
+     (when (string-match "\\[\\([0-9]+\\)|\\(\\sw+\\)\\]" lastprompt)
+           (list (string-to-number (match-string 1 lastprompt))
+                 (if (equal (match-string 2 lastprompt) "weakcheck") t nil)))))
+
+(defun easycrypt-last-prompt-info-safe ()
+  "Take from `proof-shell-last-prompt' the last information in the prompt."
+  (easycrypt-last-prompt-info proof-shell-last-prompt))
+
+(defun easycrypt-set-state-infos ()
+  "Set information necessary for backtracking."
+  (if proof-shell-last-prompt
+     ;; infos = prompt infos of the very last prompt
+     ;; sp    = last locked span, which we want to fill with prompt infos
+     (let ((sp    (if proof-script-buffer (proof-last-locked-span)))
+           (infos (or (easycrypt-last-prompt-info-safe) '(0 nil))))
+
+       (unless (or (not sp) (easycrypt-get-span-statenum sp))
+         (easycrypt-set-span-statenum sp easycrypt-last-but-one-statenum))
+       (setq easycrypt-last-but-one-statenum (car infos))
+       (setq easycrypt-proof-weak-mode (car (cdr infos)))
+     )))
+
+(add-hook 'proof-state-change-hook 'easycrypt-set-state-infos)
+
+(defun easycrypt-find-and-forget (span)
+  (let ((span-staten (easycrypt-get-span-statenum span)))
+       (list (format "undo %s." (int-to-string span-staten)))))
+
+(provide 'easycrypt-hooks)
diff --git a/easycrypt/easycrypt-keywords.el b/easycrypt/easycrypt-keywords.el
new file mode 100644
index 00000000..0bc10346
--- /dev/null
+++ b/easycrypt/easycrypt-keywords.el
@@ -0,0 +1,175 @@
+;; --------------------------------------------------------------------
+;; Copyright (c) - 2012--2016 - IMDEA Software Institute
+;; Copyright (c) - 2012--2016 - Inria
+;;
+;; Distributed under the terms of the GPL-v3 license
+;; --------------------------------------------------------------------
+
+; Generated on Thu Dec 17 16:14:05 2015
+
+(defvar easycrypt-bytac-keywords '(
+  "exact"
+  "assumption"
+  "smt"
+  "by"
+  "reflexivity"
+  "done"
+))
+
+(defvar easycrypt-dangerous-keywords '(
+  "admit"
+  "admitted"
+))
+
+(defvar easycrypt-global-keywords '(
+  "axiom"
+  "axiomatized"
+  "lemma"
+  "realize"
+  "proof"
+  "qed"
+  "abort"
+  "goal"
+  "end"
+  "import"
+  "export"
+  "include"
+  "local"
+  "declare"
+  "hint"
+  "nosmt"
+  "module"
+  "of"
+  "const"
+  "op"
+  "pred"
+  "notation"
+  "abbrev"
+  "require"
+  "theory"
+  "abstract"
+  "section"
+  "type"
+  "class"
+  "instance"
+  "print"
+  "search"
+  "as"
+  "Pr"
+  "clone"
+  "with"
+  "rename"
+  "prover"
+  "timeout"
+  "why3"
+  "dump"
+  "remove"
+  "Top"
+  "Self"
+))
+
+(defvar easycrypt-internal-keywords '(
+  "time"
+  "undo"
+  "debug"
+  "pragma"
+))
+
+(defvar easycrypt-prog-keywords '(
+  "forall"
+  "exists"
+  "fun"
+  "glob"
+  "let"
+  "in"
+  "var"
+  "proc"
+  "if"
+  "then"
+  "else"
+  "elif"
+  "while"
+  "assert"
+  "return"
+  "res"
+  "equiv"
+  "hoare"
+  "phoare"
+  "islossless"
+))
+
+(defvar easycrypt-tactic-keywords '(
+  "beta"
+  "iota"
+  "zeta"
+  "eta"
+  "logic"
+  "delta"
+  "simplify"
+  "congr"
+  "change"
+  "split"
+  "left"
+  "right"
+  "case"
+  "pose"
+  "cut"
+  "have"
+  "suff"
+  "elim"
+  "clear"
+  "apply"
+  "rewrite"
+  "rwnormal"
+  "subst"
+  "progress"
+  "trivial"
+  "auto"
+  "idtac"
+  "move"
+  "modpath"
+  "field"
+  "fieldeq"
+  "ring"
+  "ringeq"
+  "algebra"
+  "transitivity"
+  "symmetry"
+  "seq"
+  "wp"
+  "sp"
+  "sim"
+  "skip"
+  "call"
+  "rcondt"
+  "rcondf"
+  "swap"
+  "cfold"
+  "rnd"
+  "pr_bounded"
+  "bypr"
+  "byphoare"
+  "byequiv"
+  "fel"
+  "conseq"
+  "exfalso"
+  "inline"
+  "alias"
+  "fission"
+  "fusion"
+  "unroll"
+  "splitwhile"
+  "kill"
+  "eager"
+))
+
+(defvar easycrypt-tactical-keywords '(
+  "try"
+  "first"
+  "last"
+  "do"
+  "strict"
+  "expect"
+))
+
+(provide 'easycrypt-keywords)
diff --git a/easycrypt/easycrypt-syntax.el b/easycrypt/easycrypt-syntax.el
new file mode 100644
index 00000000..a784395b
--- /dev/null
+++ b/easycrypt/easycrypt-syntax.el
@@ -0,0 +1,178 @@
+;; --------------------------------------------------------------------
+;; Copyright (c) - 2012--2016 - IMDEA Software Institute
+;; Copyright (c) - 2012--2016 - Inria
+;;
+;; Distributed under the terms of the GPL-v3 license
+;; --------------------------------------------------------------------
+
+(require 'proof-syntax)
+(require 'easycrypt-keywords)
+(require 'easycrypt-hooks)
+
+(defconst easycrypt-id "[A-Za-z_]+")
+
+(defconst easycrypt-terminal-string    ".")
+(defconst easycrypt-command-end-regexp "[^\\.]\\.\\(\\s \\|\n\\|$\\)")
+
+(defconst easycrypt-keywords-proof-goal '("lemma" "equiv" "hoare" "realize"))
+(defconst easycrypt-keywords-proof-save '("save" "qed"))
+
+(defconst easycrypt-non-undoables-regexp "^pragma\\b")
+
+(defconst easycrypt-keywords-code-open  '("{"))
+(defconst easycrypt-keywords-code-close '("}")) 
+(defconst easycrypt-keywords-code-end   '(";"))
+
+(defvar easycrypt-other-symbols "\\(\\.\\.\\|\\[\\]\\)")
+
+(defvar easycrypt-operator-char-1 "=\\|<\\|>\\|~")
+(defvar easycrypt-operator-char-2 "\\+\\|\\-")
+(defvar easycrypt-operator-char-3 "\\*\\|/\\|%")
+(defvar easycrypt-operator-char-4 "!\\|\\$\\|&\\|\\?\\|@\\|\\^\\|:\\||\\|#")
+
+(defvar easycrypt-operator-char-1234
+  (concat "\\(" easycrypt-operator-char-1
+          "\\|" easycrypt-operator-char-2
+		  "\\|" easycrypt-operator-char-3
+		  "\\|" easycrypt-operator-char-4
+          "\\)"))
+
+(defconst easycrypt-proof-save-regexp
+  (concat "^\\(" (proof-ids-to-regexp easycrypt-keywords-proof-save) "\\)\\b"))
+
+(defconst easycrypt-goal-command-regexp
+  (concat "^\\(?:local\\s-+\\)?\\(?:" (proof-ids-to-regexp easycrypt-keywords-proof-goal) "\\)"
+          "\\s-+\\(?:nosmt\\s-+\\)?\\(\\sw+\\)"))
+
+(defun easycrypt-save-command-p (span str)
+  "Decide whether argument is a [save|qed] command or not"
+  (let ((txt (or (span-property span 'cmd) "")))
+       (proof-string-match-safe easycrypt-proof-save-regexp txt)))
+
+(defun easycrypt-goal-command-p (span)
+  "Is SPAN a goal start?"
+  (let ((txt (or (span-property span 'cmd) "")))
+       (proof-string-match-safe easycrypt-goal-command-regexp txt)))
+
+(defun easycrypt-init-output-syntax-table ()
+  "Set appropriate values for syntax table for EasyCrypt output."
+  (modify-syntax-entry ?,   " ")
+  (modify-syntax-entry ?\'  "_")
+  (modify-syntax-entry ?_   "_")
+
+  ;; For comments
+  (modify-syntax-entry ?\* ". 23") 
+
+  ;; For blocks
+  (modify-syntax-entry ?\( "()1")
+  (modify-syntax-entry ?\) ")(4")
+  (modify-syntax-entry ?\{ "(}")
+  (modify-syntax-entry ?\} "){")
+  (modify-syntax-entry ?\[ "(]")
+  (modify-syntax-entry ?\] ")["))
+
+;; ----- regular expressions
+
+(defvar easycrypt-error-regexp "^\\[error-[0-9]+-[0-9]+\\]\\|^anomaly"
+  "A regexp indicating that the EasyCrypt process has identified an error.")
+
+(defvar easycrypt-shell-proof-completed-regexp "No more goals"
+  "*Regular expression indicating that the proof has been completed.")
+
+(defconst easycrypt-any-command-regexp
+  ;; allow terminator to be considered as command start:
+  ;; FIXME: really needs change in generic function to take account of this,
+  ;; since the end character of a command is not the start
+  (concat "\\(\\s(\\|\\s)\\|\\sw\\|\\s \\|\\s_\\)*="  ;match assignments
+          "\\|;;\\|;\\|" 
+          (proof-ids-to-regexp easycrypt-global-keywords))
+  "Regexp matching any EasyCrypt command start or the terminator character.")
+
+(defconst easycrypt-keywords-indent-open
+  (append (append '("local") easycrypt-keywords-proof-goal)
+          easycrypt-keywords-code-open))
+
+(defconst easycrypt-keywords-indent-close
+  (append easycrypt-keywords-proof-save
+          easycrypt-keywords-code-close))
+
+(defconst easycrypt-keywords-indent-enclose
+  (append easycrypt-keywords-code-open
+          easycrypt-keywords-code-close
+          easycrypt-keywords-code-end
+          easycrypt-keywords-proof-goal
+          easycrypt-keywords-proof-save))
+
+; Regular expression for indentation
+(defconst easycrypt-indent-any-regexp
+  (proof-regexp-alt easycrypt-any-command-regexp "\\s(" "\\s)"))
+    
+(defconst easycrypt-indent-enclose-regexp
+  (proof-regexp-alt (proof-ids-to-regexp easycrypt-keywords-indent-enclose) "\\s)"))
+
+(defconst easycrypt-indent-open-regexp
+  (proof-regexp-alt (proof-ids-to-regexp easycrypt-keywords-indent-open) "\\s("))
+
+(defconst easycrypt-indent-close-regexp
+  (proof-regexp-alt (proof-ids-to-regexp easycrypt-keywords-indent-close) "\\s)"))
+
+(defface easycrypt-tactics-closing-face
+  (proof-face-specs
+   (:foreground "red")
+   (:foreground "red")
+   ())
+  "Face for names of closing tactics in proof scripts."
+  :group 'proof-faces)
+
+(defface easycrypt-tactics-dangerous-face
+  (proof-face-specs
+   (:background "red")
+   (:background "red")
+   ())
+  "Face for names of dangerous tactics in proof scripts."
+  :group 'proof-faces)
+
+(defface easycrypt-tactics-tacticals-face
+  (proof-face-specs
+   (:foreground "dark green")
+   (:foreground "dark green")
+   ())
+  "Face for names of tacticals in proof scripts."
+  :group 'proof-faces)
+
+(defconst easycrypt-tactics-closing-face   'easycrypt-tactics-closing-face)
+(defconst easycrypt-tactics-dangerous-face 'easycrypt-tactics-dangerous-face)
+(defconst easycrypt-tactics-tacticals-face 'easycrypt-tactics-tacticals-face)
+
+(defvar easycrypt-font-lock-keywords
+  (list
+    (cons (proof-ids-to-regexp easycrypt-global-keywords)    'font-lock-keyword-face)
+    (cons (proof-ids-to-regexp easycrypt-tactic-keywords)    'proof-tactics-name-face)
+    (cons (proof-ids-to-regexp easycrypt-tactical-keywords)  'easycrypt-tactics-tacticals-face)
+    (cons (proof-ids-to-regexp easycrypt-bytac-keywords)     'easycrypt-tactics-closing-face)
+    (cons (proof-ids-to-regexp easycrypt-dangerous-keywords) 'easycrypt-tactics-dangerous-face)
+    (cons (proof-ids-to-regexp easycrypt-prog-keywords)      'font-lock-keyword-face)
+    (cons (concat easycrypt-operator-char-1234 "+")          'font-lock-type-face)
+    (cons easycrypt-other-symbols                            'font-lock-type-face)))
+
+(defun easycrypt-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 ?\. ".")
+  (modify-syntax-entry ?\* ". 23n")
+  (modify-syntax-entry ?\( "()1")
+  (modify-syntax-entry ?\) ")(4"))
+
+(provide 'easycrypt-syntax)
diff --git a/easycrypt/easycrypt.el b/easycrypt/easycrypt.el
new file mode 100644
index 00000000..ecea9744
--- /dev/null
+++ b/easycrypt/easycrypt.el
@@ -0,0 +1,265 @@
+;; --------------------------------------------------------------------
+;; Copyright (c) - 2012--2016 - IMDEA Software Institute
+;; Copyright (c) - 2012--2016 - Inria
+;;
+;; Distributed under the terms of the GPL-v3 license
+;; --------------------------------------------------------------------
+
+(require 'proof)
+(require 'pg-custom)
+(require 'easycrypt-syntax)
+(require 'easycrypt-hooks)
+(require 'easycrypt-abbrev)
+
+(add-to-list 'hs-special-modes-alist
+  '(easycrypt-mode "{" "}" "/[*/]" nil nil))
+
+;; --------------------------------------------------------------------
+(defun easycrypt-load-path-safep (path)
+  (and
+   (listp path)
+   (every (lambda (entry) (stringp entry)) path)))
+
+;; --------------------------------------------------------------------
+(defcustom easycrypt-prog-name "easycrypt"
+  "*Name of program to run EasyCrypt."
+  :type  'file
+  :group 'easycrypt)
+
+(defcustom easycrypt-load-path nil
+  "Non-standard EasyCrypt library load path.
+This list specifies the include path for EasyCrypt. The elements of
+this list are strings."
+  :type  '(repeat (string :tag "simple directory (-I)"))
+  :safe  'easycrypt-load-path-safep
+  :group 'easycrypt)
+
+(defcustom easycrypt-web-page
+  "http://www.easycrypt.info/"
+  "URL of web page for EasyCrypt."
+  :type  'string
+  :group 'easycrypt-config)
+
+;; --------------------------------------------------------------------
+(defun easycrypt-option-of-load-path-entry (entry)
+  (list "-I" (expand-file-name entry)))
+
+;; --------------------------------------------------------------------
+(defun easycrypt-include-options ()
+  (let ((result nil))
+    (when easycrypt-load-path
+      (dolist (entry easycrypt-load-path)
+        (setq result (append result (easycrypt-option-of-load-path-entry entry)))))
+    result))
+
+;; --------------------------------------------------------------------
+(defun easycrypt-build-prog-args ()
+  (delete "-emacs" easycrypt-prog-args)
+  (push "-emacs" easycrypt-prog-args))
+
+(easycrypt-build-prog-args)
+
+;; --------------------------------------------------------------------
+(defun easycrypt-prog-args ()
+  (message "%s" easycrypt-load-path)
+  (append easycrypt-prog-args (easycrypt-include-options)))
+
+;; --------------------------------------------------------------------
+;; Generic mode
+
+(defun easycrypt-config ()
+  "Configure Proof General scripting for EasyCrypt."
+  (easycrypt-init-output-syntax-table)
+  
+  (setq  proof-terminal-string                 easycrypt-terminal-string)
+  (setq  proof-script-command-end-regexp       easycrypt-command-end-regexp)
+
+  (setq  proof-script-comment-start            "(*"
+         proof-script-comment-end              "*)")
+  
+  ;; For undo
+  (setq  proof-find-and-forget-fn              'easycrypt-find-and-forget
+         proof-completed-proof-behaviour       nil
+         proof-non-undoables-regexp            easycrypt-non-undoables-regexp
+         proof-shell-restart-cmd               "pragma restart. ")
+
+  (set (make-local-variable 'comment-quote-nested) nil)
+
+  ;; For func-menu and finding goal...save regions
+  (setq  proof-save-command-regexp             easycrypt-proof-save-regexp
+         proof-really-save-command-p           'easycrypt-save-command-p
+         proof-save-with-hole-regexp           nil
+         proof-goal-command-p                  'easycrypt-goal-command-p
+         proof-goal-with-hole-regexp           easycrypt-goal-command-regexp
+         proof-goal-with-hole-result           1)
+
+  (setq  proof-goal-command                    "lemma %s: ."
+         proof-save-command                    "qed.")
+  
+  (setq  proof-prog-name                       easycrypt-prog-name
+         proof-assistant-home-page             easycrypt-web-page)
+
+  ; Options
+  (setq  proof-three-window-enable             t
+         proof-three-window-mode-policy        (quote hybrid)
+         proof-auto-multiple-files             t)
+
+  ; Setting indents 
+  (set   (make-local-variable 'indent-tabs-mode) nil)
+  (setq  proof-indent-enclose-offset   (- proof-indent)
+         proof-indent-open-offset     0
+         proof-indent-close-offset    0
+         proof-indent-any-regexp      easycrypt-indent-any-regexp
+         proof-indent-enclose-regexp  easycrypt-indent-enclose-regexp
+         proof-indent-open-regexp     easycrypt-indent-open-regexp
+         proof-indent-close-regexp    easycrypt-indent-close-regexp)
+
+  ; Silent/verbose mode for batch processing
+  (setq proof-shell-start-silent-cmd "pragma silent. "
+        proof-shell-stop-silent-cmd  "pragma verbose. ")
+
+  ; Ask for the current goal
+  (setq proof-showproof-command "pragma noop. ")
+
+  (easycrypt-init-syntax-table)
+  ;; we can cope with nested comments
+  (set (make-local-variable 'comment-quote-nested) nil)
+
+  (setq  proof-script-font-lock-keywords
+         easycrypt-font-lock-keywords))
+
+(defun easycrypt-shell-config ()
+  "Configure Proof General shell for EasyCrypt."
+  (easycrypt-init-output-syntax-table)
+  (setq  proof-shell-auto-terminate-commands    easycrypt-terminal-string)
+  (setq  proof-shell-eager-annotation-start
+     (concat "\\(?:^\\[W\\] *\\)\\|\\(?:" easycrypt-shell-proof-completed-regexp "\\)"))
+  (setq  proof-shell-strip-crs-from-input       nil)
+  (setq  proof-shell-annotated-prompt-regexp    "^\\[[0-9]+|\\sw+\\]>")
+  (setq  proof-shell-clear-goals-regexp         easycrypt-shell-proof-completed-regexp)
+  (setq  proof-shell-proof-completed-regexp     easycrypt-shell-proof-completed-regexp)
+  (setq  proof-shell-error-regexp               easycrypt-error-regexp)
+  (setq  proof-shell-truncate-before-error      nil)
+  (setq  proof-shell-start-goals-regexp         "^Current")
+  (setq  proof-shell-end-goals-regexp           nil)  ; up to next prompt
+  (setq  proof-shell-font-lock-keywords         easycrypt-font-lock-keywords))
+
+;; --------------------------------------------------------------------
+;; Derived modes
+
+(define-derived-mode easycrypt-mode proof-mode
+  "EasyCrypt script" nil
+  (easycrypt-config)
+  (proof-config-done))
+
+(define-derived-mode easycrypt-shell-mode proof-shell-mode
+  "EasyCrypt shell" nil
+  (easycrypt-shell-config)
+  (proof-shell-config-done))
+
+(define-derived-mode easycrypt-response-mode proof-response-mode
+  "EasyCrypt response" nil
+  (easycrypt-init-output-syntax-table)
+  (setq  proof-response-font-lock-keywords 
+         easycrypt-font-lock-keywords)
+  (proof-response-config-done))
+
+(define-derived-mode easycrypt-goals-mode proof-goals-mode
+  "EasyCrypt goals" nil
+  (easycrypt-init-output-syntax-table)
+  (setq  proof-goals-font-lock-keywords 
+         easycrypt-font-lock-keywords)
+  (proof-goals-config-done))
+
+(defun easycrypt-get-last-error-location () 
+  "Remove [error] in the error message and extract the position
+  and length of the error "
+  (proof-with-current-buffer-if-exists proof-response-buffer
+
+     (goto-char (point-max))
+     (when (re-search-backward "\\[error-\\([0-9]+\\)-\\([0-9]+\\)\\]" nil t)
+        (let* ((inhibit-read-only t)
+               (pos1 (string-to-number (match-string 1)))
+               (pos2 (string-to-number (match-string 2)))
+               (len (- pos2 pos1)))
+
+              (delete-region (match-beginning 0) (match-end 0))
+              (list pos1 len)))))
+
+(defun easycrypt-advance-until-command ()
+   (while (proof-looking-at "\\s-") (forward-char 1)))
+
+(defun easycrypt-highlight-error ()
+  "Use 'easycrypt-get-last-error-location' to know the position
+  of the error and then highlight in the script buffer"
+  (proof-with-current-buffer-if-exists proof-script-buffer
+    (let ((mtch (easycrypt-get-last-error-location)))
+        (when mtch
+          (let ((pos (car mtch))
+                  (lgth (cadr mtch)))
+          (if (eq (proof-unprocessed-begin) (point-min))
+                (goto-char (proof-unprocessed-begin))
+                (goto-char (+ (proof-unprocessed-begin) 1)))
+            (easycrypt-advance-until-command)
+             (goto-char (+ (point) pos))
+             (span-make-self-removing-span
+               (point) (+ (point) lgth)
+               'face 'proof-script-highlight-error-face))))))
+
+(defun easycrypt-highlight-error-hook ()
+  (easycrypt-highlight-error))
+
+(defun easycrypt-redisplay-hook ()
+  (easycrypt-redisplay))
+
+(add-hook 'proof-shell-handle-error-or-interrupt-hook
+          'easycrypt-highlight-error-hook t)
+
+;; --------------------------------------------------------------------
+;; Check mode related commands
+(defun easycrypt-cmode-check ()
+  "Set EasyCrypt in check mode."
+  (interactive)
+  (proof-shell-invisible-command "pragma Proofs:check."))
+
+(defun easycrypt-cmode-weak-check ()
+  "Set EasyCrypt in weak-check mode."
+  (interactive)
+  (proof-shell-invisible-command "pragma Proofs:weak."))
+
+;; --------------------------------------------------------------------
+(defun easycrypt-ask-do (do)
+  (let* ((cmd))
+    (setq cmd (read-string (format "Term for `%s': " do)))
+    (proof-shell-ready-prover)
+    (proof-shell-invisible-command (format " %s %s . " do cmd))))
+
+;; --------------------------------------------------------------------
+(defun easycrypt-Print ()
+  "Ask for a term and print its type."
+  (interactive)
+  (easycrypt-ask-do "print"))
+
+;; --------------------------------------------------------------------
+(defun easycrypt-Check ()
+  (easycrypt-Print))
+
+;; --------------------------------------------------------------------
+;; Key bindings
+
+(define-key easycrypt-keymap "\C-p" 'easycrypt-Print)
+(define-key easycrypt-goals-mode-map "\C-c\C-a\C-p" 'easycrypt-Print)
+(define-key easycrypt-response-mode-map "\C-c\C-a\C-p" 'easycrypt-Print)
+
+(define-key easycrypt-keymap "\C-c" 'easycrypt-Check)
+(define-key easycrypt-goals-mode-map "\C-c\C-a\C-c" 'easycrypt-Check)
+(define-key easycrypt-response-mode-map "\C-c\C-a\C-c" 'easycrypt-Check)
+
+;; --------------------------------------------------------------------
+;; 3-window pane layout hack
+(add-hook
+  'proof-activate-scripting-hook
+  '(lambda () (when proof-three-window-enable (proof-layout-windows))))
+
+;; --------------------------------------------------------------------
+(provide 'easycrypt)
diff --git a/etc/desktop/icons/128x128/proofgeneral.png b/etc/desktop/icons/128x128/proofgeneral.png
new file mode 100644
index 00000000..555e4a87
--- /dev/null
+++ b/etc/desktop/icons/128x128/proofgeneral.png
diff --git a/etc/desktop/icons/64x64/proofgeneral.png b/etc/desktop/icons/64x64/proofgeneral.png
new file mode 100644
index 00000000..15492240
--- /dev/null
+++ b/etc/desktop/icons/64x64/proofgeneral.png
diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el
index bb765c2c..4958b360 100644
--- a/generic/pg-pamacs.el
+++ b/generic/pg-pamacs.el
@@ -228,7 +228,9 @@ which can be changed by sending commands.
 In this case, NAME stands for the internal setting, flag, etc,
 for the proof assistant, and a :setting and :type value should be
 provided.  The :type of NAME should be one of 'integer, 'float,
-'boolean, 'string.
+'boolean, 'string. Other types are not supported (see
+`proof-menu-entry-for-setting'). They will yield an error when
+constructing the proof assistant menu.
 
 The function `proof-assistant-format' is used to format VAL.
 
diff --git a/generic/pg-vars.el b/generic/pg-vars.el
index 3aafa97d..8d93a60b 100644
--- a/generic/pg-vars.el
+++ b/generic/pg-vars.el
@@ -209,7 +209,25 @@ and the function `proof-assistant-format'.  The TYPE item determines
 the form of the menu entry for the setting (this is an Emacs widget type)
 and the DESCR description string is used as a help tooltip in the settings menu.
 
-This list is extended by the `defpacustom' macro.")
+As TYPE's only the simple types boolean, integer, number and
+string are supported (see `proof-menu-entry-for-setting'). Other
+types will yield an error when constructing the proof assistant
+menu from this list.
+
+Customizations defined with `defpacustom' are automatically added
+to this list.")
+
+(defvar proof-assistant-additional-settings nil
+  "Additional proof assistant specific customizations (as list of symbols).
+This variable should hold those proof assistant specific
+customizations that are not included in
+`proof-assistant-settings' but which should be saved/restored
+with the save and reset settings menu entry in the proof
+assistant menu.
+
+Customization variables are missing in `proof-assistant-settings'
+when they have a type not supported by `defpacusom'.")
+
 
 (defvar pg-tracing-slow-mode nil
   "Non-nil for slow refresh mode for tracing output.")
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index d4e0f803..df617347 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -921,8 +921,10 @@ KEY is the optional key binding."
 
 (defun proof-settings-vars ()
   "Return a list of proof assistant setting variables."
-  (mapcar (lambda (setting) (proof-ass-symv (car setting)))
-	  proof-assistant-settings))
+  (append
+   (mapcar (lambda (setting) (proof-ass-symv (car setting)))
+	   proof-assistant-settings)
+   proof-assistant-additional-settings))
 
 (defun proof-settings-changed-from-defaults-p ()
   ;; FIXME: would be nice to add.  Custom support?
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 51038fa6..13da8d98 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -831,7 +831,11 @@ the prover command buffer (e.g., with Isabelle2009 press RET inside *isabelle*).
   (let ((prover-was-busy nil))
     (unless (proof-shell-live-buffer)
       (error "Proof process not started!"))
-    ;; hook functions might set prover-was-busy
+    ;; Hook functions might set prover-was-busy.
+    ;; In case `proof-action-list' is empty and only
+    ;; `proof-second-action-list-active' is t, the hook functions
+    ;; should clear the queue region and release the proof shell lock.
+    ;; `coq-par-user-interrupt' actually does this.
     (run-hooks 'proof-shell-signal-interrupt-hook)
     (if proof-shell-busy
 	(progn
diff --git a/generic/proof-site.el b/generic/proof-site.el
index c2f9f480..671c3c82 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -39,10 +39,11 @@
 
       (isar "Isabelle" "thy")
       (coq "Coq" "v" nil (".vo" ".glob"))
-      (phox "PhoX" "phx")
+      (easycrypt "EasyCrypt" "ec" ".*\\.eca?")
 
       ;; Obscure instances or conflict with other Emacs modes.
 
+      ;; (phox "PhoX" "phx")
       ;; (lego "LEGO" "l")
       ;; (ccc    "CASL Consistency Checker" "ccc")
 
diff --git a/generic/proof-tree.el b/generic/proof-tree.el
index 77d3cc33..f0894656 100644
--- a/generic/proof-tree.el
+++ b/generic/proof-tree.el
@@ -842,13 +842,14 @@ The not yet delayed output is in the region
 	 (start proof-shell-delayed-output-start)
 	 (end proof-shell-delayed-output-end)
 	 inst-ex-vars)
-    (when (and (not (memq 'proof-tree-show-subgoal flags))
-	       (> state proof-tree-last-state))
-      ;; Only deal with existentials if the proof assistant has them
-      ;; (i.e., proof-tree-existential-regexp is set) and if there are some
-      ;; goals with existentials.
-      (when (and proof-tree-existential-regexp
+    (unless (memq 'proof-tree-show-subgoal flags)
+      (when (and (> state proof-tree-last-state)
+		 proof-tree-existential-regexp
 		 proof-tree-existentials-alist)
+	;; Only deal with existentials if this is not and undo
+	;; command, if the proof assistant actually has existentials
+	;; (i.e., proof-tree-existential-regexp is set) and if there
+	;; are some goals with existentials.
 	(setq inst-ex-vars
 	      (with-current-buffer proof-shell-buffer
 		(funcall proof-tree-extract-instantiated-existentials