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

5 files changed, 37 insertions, 2 deletions

diff --git a/.travis.yml b/.travis.yml
index d0649dce..6f70e507 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -7,6 +7,7 @@ env:
   - EMACS_TARGET=emacs-24.5
   - EMACS_TARGET=emacs-25.1
   - EMACS_TARGET=emacs-25.2
+  - EMACS_TARGET=emacs-25.3
 
 before_install:
   - make -f Makefile.travis before_install
diff --git a/Makefile.travis b/Makefile.travis
index 1393a1e8..57efb391 100644
--- a/Makefile.travis
+++ b/Makefile.travis
@@ -1,4 +1,4 @@
-VERSIONS = 24.1 24.2 24.3 24.4 24.5 25.1 25.2
+VERSIONS = 24.1 24.2 24.3 24.4 24.5 25.1 25.2 25.3
 STABLE_TARGETS = $(addprefix prepare-emacs-,$(VERSIONS))
 
 .PHONY: prepare-emacs-24 prepare-emacs-git $(STABLE_TARGETS) \
diff --git a/README.md b/README.md
index 77dddcf1..1a2b8266 100644
--- a/README.md
+++ b/README.md
@@ -2,12 +2,28 @@
 
 [![Build Status](https://travis-ci.org/ProofGeneral/PG.svg?branch=master)](https://travis-ci.org/ProofGeneral/PG)
 
+## Overview
+
 Proof General is a generic Emacs interface for proof assistants.
 The aim of the Proof General project is to provide a powerful, generic
 environment for using interactive proof assistants.
 
 This is version 4.4.1~pre of Proof General.
 
+## About Proof General branches
+
+Two editions of Proof General are currently available:
+
+* the (legacy) REPL-based, stable version of Proof General,
+  gathered in the
+  [master](https://github.com/ProofGeneral/PG/tree/master) branch, and
+  licensed under GPLv2;
+* the (newest) Coq-specific, experimental version of Proof General,
+  supporting asynchronous proof processing,
+  gathered in the
+  [async](https://github.com/ProofGeneral/PG/tree/async) branch, and
+  licensed under GPLv3+.
+
 ## Setup
 
 Remove old versions of Proof General, then download and install the new release from GitHub:
@@ -57,3 +73,12 @@ Supported proof assistants:
 * Obsolete instances: Demoisa, Lambda-Clam, Plastic
 
 A few example proofs are included in each prover subdirectory.
+
+## Contributing
+
+Contributions to this repository are placed under the BSD-3 license.
+As BSD-3 is compatible with both GPLv2 and GPLv3+, this means that
+we can merge them in both `master` and `async` branches if need be,
+using the same license as the rest of the codebase, while you keep
+all the rights on your code.
+For more info, see <https://opensource.org/licenses/BSD-3-Clause>.
diff --git a/coq/coq-db.el b/coq/coq-db.el
index dd9020d8..28f2ff2b 100644
--- a/coq/coq-db.el
+++ b/coq/coq-db.el
@@ -316,7 +316,7 @@ See `coq-syntax-db' for DB structure."
   :group 'proof-faces)
 
 (defface coq-symbol-face
-  '((t :inherit default-face :bold coq-bold-unicode-binders))
+  '((t :inherit font-lock-type-face :bold coq-bold-unicode-binders))
   "Face for unicode binders, by default a bold version of `font-lock-type-face'."
   :group 'proof-faces)
 
diff --git a/coq/coq-system.el b/coq/coq-system.el
index fff239c1..f3eabafc 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -33,6 +33,15 @@
   (defvar coq-prog-args)
   (defvar coq-debug))
 
+;; Arbitrary arguments can already be passed through _CoqProject.
+;; However this is not true for all assistants, so we don't modify the
+;; (defpgcustom prog-args) declaration.
+(defun coq--string-list-p (obj)
+  "Determine if OBJ is a list of strings."
+  (or (null obj) (and (consp obj) (stringp (car obj)) (coq--string-list-p (cdr obj)))))
+
+(put 'coq-prog-args 'safe-local-variable #'coq--string-list-p)
+
 (defcustom coq-prog-env nil
   "List of environment settings to pass to Coq process.
 On Windows you might need something like: