From 53950e9e57639a35d6bf542000636ff6f605acb0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Tue, 24 Oct 2017 17:21:33 +0200
Subject: Make coq-prog-args safe when list of strings.

They could be passed through _CoqProject regardless.
---
 coq/coq-system.el | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/coq/coq-system.el b/coq/coq-system.el
index 8da4ea23..0bcf6a07 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -22,6 +22,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 d to pass to Coq process.
 On Windows you might need something like:
-- 
cgit v1.2.3


From 2c12ce635fb85a709b23c8af9ef490c144383da8 Mon Sep 17 00:00:00 2001
From: Yishuai Li <yishuai@cis.upenn.edu>
Date: Sun, 11 Mar 2018 23:57:41 -0400
Subject: CI Emacs 25.3

---
 .travis.yml     | 1 +
 Makefile.travis | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

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) \
-- 
cgit v1.2.3


From 10a17a7142474a392427d600ef3f0eaa7bc0f478 Mon Sep 17 00:00:00 2001
From: stardiviner <numbchild@gmail.com>
Date: Tue, 17 Apr 2018 15:47:17 +0800
Subject: small fix of face `coq-symbol-face'

---
 coq/coq-db.el | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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)
 
-- 
cgit v1.2.3


From 75283fdbb3c9179730091ec7076b37a9bcb86dad Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel <erik@martin-dorel.org>
Date: Tue, 29 May 2018 00:09:59 +0200
Subject: Add note about PG branches and license

---
 README.md | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

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>.
-- 
cgit v1.2.3