12 files changed, 130 insertions, 41 deletions
diff --git a/dev/README b/dev/README
index 6b83579def..453f85f0d6 100644
--- a/dev/README
+++ b/dev/README
@@ -40,7 +40,11 @@ Documentation of ML interfaces using ocamldoc (directory ocamldoc/html)
 Other development tools (directory tools)
 -----------------------
 
+coqdev.el: helper customizations for everyday Coq development, eg
+  making `compile' work in subdirectories
+
 objects.el: various development utilities at emacs level
+
 anomaly-traces-parser.el: a .emacs-ready elisp snippet to parse
   location of Anomaly backtraces and jump to them conveniently from
   the Emacs *compilation* output.
diff --git a/dev/base_include b/dev/base_include
index 472c0c605e..350ccaa109 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -19,7 +19,6 @@
 #directory "stm";;
 #directory "vernac";;
 
-#directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *)
 #directory "+camlp5";; (* Gramext is found in top_printers.ml *)
 
 #use "top_printers.ml";;
@@ -230,7 +229,7 @@ let _ = Flags.in_toplevel := true
 let _ = Constrextern.set_extern_reference
   (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Id.Set.empty r));;
 
-let go () = Coqloop.loop Option.(get !Coqtop.drop_last_doc)
+let go () = Coqloop.loop ~time:false ~state:Option.(get !Coqtop.drop_last_doc)
 
 let _ =
  print_string
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index c467678215..d8cde39f82 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -794,8 +794,8 @@ function make_ocaml {
     # TODO: this might not work if PREFIX contains spaces
     sed -i "s|^PREFIX=.*|PREFIX=$PREFIXOCAML|" config/Makefile
     
-    # We don't want to mess up Coq's dirctory structure so put the OCaml library in a separate folder
-    # If we refer to the make variable ${PREFIX} below, camlp4 ends up having a wrong path:
+    # We don't want to mess up Coq's directory structure so put the OCaml library in a separate folder
+    # If we refer to the make variable ${PREFIX} below, camlp5 ends up having the wrong path:
     # D:\bin\coq64_buildtest_abs_ocaml4\bin>ocamlc -where => D:/bin/coq64_buildtest_abs_ocaml4/libocaml
     # D:\bin\coq64_buildtest_abs_ocaml4\bin>camlp4 -where => ${PREFIX}/libocaml\camlp4
     # So we put an explicit path in there
diff --git a/dev/core.dbg b/dev/core.dbg
index 00a4355a48..57c136900d 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -1,4 +1,4 @@
-source camlp4.dbg
+source camlp5.dbg
 load_printer threads.cma
 load_printer str.cma
 load_printer clib.cma
diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt
index f3fc13e969..abba13428f 100644
--- a/dev/doc/build-system.dev.txt
+++ b/dev/doc/build-system.dev.txt
@@ -46,7 +46,7 @@ see build-system.txt .
 .ml4 files
 ----------
 
-.ml4 are converted to .ml by camlp4. By default, they are produced
+.ml4 are converted to .ml by camlp5. By default, they are produced
 in the binary ast format understood by ocamlc/ocamlopt/ocamldep.
 Pros:
  - faster than parsing clear-text source file.
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index 873adc1b22..1c4fd2eba4 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -88,7 +88,7 @@ bootstrapped. The dependencies of a file FOO are in FOO.d . This
 enables partial recalculation of dependencies (only the dependencies
 of changed files are recomputed).
 
-If you add a dependency to a Coq camlp4 extension (grammar.cma or
+If you add a dependency to a Coq camlp5 extension (grammar.cma or
 q_constr.cmo), then see sections ".ml4 files" and "new files".
 
 Cleaning Targets
@@ -127,7 +127,7 @@ of a grammar extension via a line of the form:
 
 The use of (*i camlp4use: ... i*) to mention uses of standard
 extension such as IFDEF has also been discontinued, the Makefile now
-always calls camlp4 with pa_macros.cmo and a few others by default.
+always calls camlp5 with pa_macros.cmo and a few others by default.
 
 For debugging a Coq grammar extension, it could be interesting
 to use the READABLE_ML4=1 option, otherwise the generated .ml are
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index aef62b0092..16a31790a4 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -20,6 +20,14 @@ General deprecation
   removed. Please, make sure your plugin is warning-free in 8.7 before
   trying to port it over 8.8.
 
+Proof engine
+
+  Due to the introduction of `EConstr` in 8.7, it is not necessary to
+  track "goal evar normal form status" anymore, thus the type `'a
+  Proofview.Goal.t` loses its ghost argument. This may introduce some
+  minor incompatibilities at the typing level. Code-wise, things
+  should remain the same.
+
 We removed the following functions:
 
 - `Universes.unsafe_constr_of_global`: use `Global.constr_of_global_in_context`
diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt
index 2dbd132da7..b3d49b7e56 100644
--- a/dev/doc/coq-src-description.txt
+++ b/dev/doc/coq-src-description.txt
@@ -25,7 +25,7 @@ intf :
 
 grammar :
 
- Camlp4 syntax extensions. The file grammar/grammar.cma is used
+ Camlp5 syntax extensions. The file grammar/grammar.cma is used
  to pre-process .ml4 files containing EXTEND constructions,
  either TACTIC EXTEND, ARGUMENTS EXTEND or VERNAC ... EXTEND.
  This grammar.cma incorporates many files from other directories
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index 3cbccab44c..f3e60edea8 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -3,19 +3,19 @@
 # Wrapper around ocamldebug for Coq
 
 # This file is to be launched via the generated script ocamldebug-coq,
-# which will set the env variables $OCAMLDEBUG, $CAMLP4LIB, $COQTOP
+# which will set the env variables $OCAMLDEBUG, $CAMLP5LIB, $COQTOP
 # Anyway, just in case someone tries to use this script directly,
 # here are some reasonable default values
 
 [ -z "$OCAMLDEBUG" ] && OCAMLDEBUG=ocamldebug
-[ -z "$CAMLP4LIB" ] && CAMLP4LIB=+camlp5
+[ -z "$CAMLP5LIB" ] && CAMLP5LIB=+camlp5
 [ -z "$COQTOP" -a -d "$PWD/kernel" ] && COQTOP=$PWD
 [ -z "$COQTOP" -a -d "$PWD/../kernel" ] && COQTOP=`dirname $PWD`
 
 export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH
 
 exec $OCAMLDEBUG \
-	-I $CAMLP4LIB -I +threads \
+	-I $CAMLP5LIB -I +threads \
 	-I $COQTOP \
 	-I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \
 	-I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \
diff --git a/dev/tools/anomaly-traces-parser.el b/dev/tools/anomaly-traces-parser.el
deleted file mode 100644
index 68f54266f9..0000000000
--- a/dev/tools/anomaly-traces-parser.el
+++ /dev/null
@@ -1,28 +0,0 @@
-;; This Elisp snippet adds a regexp parser for the format of Anomaly
-;; backtraces (coqc -bt ...), to the error parser of the Compilation
-;; mode (C-c C-c: "Compile command: ..."). Once the
-;; coq-change-error-alist-for-backtraces function has run, file
-;; locations in traces are recognized and can be jumped from easily
-;; from the *compilation* buffer.
-
-;; You can just copy everything below to your .emacs and this will be
-;; enabled from any compilation command launched from an OCaml file.
-
-(defun coq-change-error-alist-for-backtraces ()
-  "Hook to change the compilation-error-regexp-alist variable, to
-   search the coq backtraces for error locations"
-  (interactive)
-  (add-to-list
-   'compilation-error-regexp-alist-alist
-   '(coq-backtrace
-     "^ *\\(?:raise\\|frame\\) @ file \\(\"?\\)\\([^,\" \n\t<>]+\\)\\1,\
-      lines? \\([0-9]+\\)-?\\([0-9]+\\)?\\(?:$\\|,\
-      \\(?: characters? \\([0-9]+\\)-?\\([0-9]+\\)?:?\\)?\\)"
-     2 (3 . 4) (5 . 6)))
-  (add-to-list 'compilation-error-regexp-alist 'coq-backtrace))
-
-;; this Anomaly parser should be available when one is hacking
-;; on the *OCaml* code of Coq (adding bugs), so we enable it
-;; through the OCaml mode hooks.
-(add-hook 'caml-mode-hook 'coq-change-error-alist-for-backtraces)
-(add-hook 'tuareg-mode-hook 'coq-change-error-alist-for-backtraces)
diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el
new file mode 100644
index 0000000000..8c55be2831
--- /dev/null
+++ b/dev/tools/coqdev.el
@@ -0,0 +1,106 @@
+;;; coqdev.el --- Emacs helpers for Coq development  -*- lexical-binding:t -*-
+
+;; Copyright (C) 2018 The Coq Development Team
+
+;; Maintainer: coqdev@inria.fr
+
+;;; Commentary:
+
+;; Helpers to set compilation commands, proof general variables, etc
+;; for Coq development
+
+;; You can disable individual features without editing this file by
+;; using `remove-hook', for instance
+;; (remove-hook 'hack-local-variables-hook #'coqdev-setup-compile-command)
+
+;;; Installation:
+
+;; To use this, with coqdev.el located at /path/to/coqdev.el, add the
+;; following to your init:
+
+;; (add-to-list 'load-path "/path/to/coqdev/")
+;; (require 'coqdev)
+
+;; If you load this file from a git repository, checking out an old
+;; commit will make it disappear and cause errors for your Emacs
+;; startup. To ignore those errors use (require 'coqdev nil t). If you
+;; check out a malicious commit Emacs startup would allow it to run
+;; arbitrary code, to avoid this you can copy coqdev.el to any
+;; location and adjust the load path accordingly (of course if you run
+;; ./configure to compile Coq it is already too late).
+
+;;; Code:
+
+(defun coqdev-default-directory ()
+  "Return the Coq repository containing `default-directory'."
+  (let ((dir (locate-dominating-file default-directory "META.coq")))
+    (when dir (expand-file-name dir))))
+
+(defun coqdev-setup-compile-command ()
+  "Setup `compile-command' for Coq development."
+  (let ((dir (coqdev-default-directory)))
+    (when dir (setq-local compile-command (concat "make -C " (shell-quote-argument dir))))))
+(add-hook 'hack-local-variables-hook #'coqdev-setup-compile-command)
+
+(defvar camldebug-command-name) ; from camldebug.el (caml package)
+(defvar ocamldebug-command-name) ; from ocamldebug.el (tuareg package)
+(defun coqdev-setup-camldebug ()
+  "Setup ocamldebug for Coq development.
+
+Specifically `camldebug-command-name' and `ocamldebug-command-name'."
+  (let ((dir (coqdev-default-directory)))
+    (when dir
+      (setq-local camldebug-command-name
+                  (concat dir "dev/ocamldebug-coq"))
+      (setq-local ocamldebug-command-name
+                  (concat dir "dev/ocamldebug-coq")))))
+(add-hook 'hack-local-variables-hook #'coqdev-setup-camldebug)
+
+(defun coqdev-setup-tags ()
+  "Setup `tags-file-name' for Coq development."
+  (let ((dir (coqdev-default-directory)))
+    (when dir (setq-local tags-file-name (concat dir "TAGS")))))
+(add-hook 'hack-local-variables-hook #'coqdev-setup-tags)
+
+(defvar coq-prog-args)
+(defvar coq-prog-name)
+
+;; Lets us detect whether there are file local variables
+;; even though PG sets it with `setq' when there's a _Coqproject.
+;; Also makes sense generally, so might make it into PG someday.
+(make-variable-buffer-local 'coq-prog-args)
+(setq-default coq-prog-args nil)
+
+(defun coqdev-setup-proofgeneral ()
+  "Setup Proofgeneral variables for Coq development.
+
+Note that this function is executed before _Coqproject is read if it exists."
+  (let ((dir (coqdev-default-directory)))
+    (when dir
+      (unless coq-prog-args
+        (setq coq-prog-args
+              `("-coqlib" ,dir "-R" ,(concat dir "plugins")
+                "Coq" "-R" ,(concat dir "theories")
+                "Coq")))
+      (setq-local coq-prog-name (concat dir "bin/coqtop")))))
+(add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral)
+
+;; This Elisp snippet adds a regexp parser for the format of Anomaly
+;; backtraces (coqc -bt ...), to the error parser of the Compilation
+;; mode (C-c C-c: "Compile command: ..."). File locations in traces
+;; are recognized and can be jumped from easily in the *compilation*
+;; buffer.
+(defvar compilation-error-regexp-alist-alist)
+(defvar compilation-error-regexp-alist)
+(with-eval-after-load 'compile
+  (add-to-list
+   'compilation-error-regexp-alist-alist
+   '(coq-backtrace
+     "^ *\\(?:raise\\|frame\\) @ file \\(\"?\\)\\([^,\" \n\t<>]+\\)\\1,\
+      lines? \\([0-9]+\\)-?\\([0-9]+\\)?\\(?:$\\|,\
+      \\(?: characters? \\([0-9]+\\)-?\\([0-9]+\\)?:?\\)?\\)"
+     2 (3 . 4) (5 . 6)))
+  (add-to-list 'compilation-error-regexp-alist 'coq-backtrace))
+
+(provide 'coqdev)
+;;; coqdev ends here
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index af38ce4b8c..f99e2593d7 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -485,7 +485,7 @@ let in_current_context f c =
   let (evmap,sign) = Pfedit.get_current_context () in
   f (fst (Constrintern.interp_constr sign evmap c))(*FIXME*)
 
-(* We expand the result of preprocessing to be independent of camlp4
+(* We expand the result of preprocessing to be independent of camlp5
 
 VERNAC COMMAND EXTEND PrintPureConstr
 | [ "PrintPureConstr" constr(c) ] -> [ in_current_context print_pure_constr c ]