From 767816eece27e6bb8cba0bbf122507bd2a3b77a1 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 1 Nov 2017 22:54:24 +0100
Subject: Using a specific function to register vernac printers.

---
 dev/doc/changes.md | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'dev')

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 6ade6576f7..b1ebec44ef 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -38,6 +38,13 @@ Some tactics and related functions now support static configurability, e.g.:
   - if None, tells to behave as told with the flag Keep Proof Equalities
   - if Some b, tells to keep proof equalities iff b is true
 
+Declaration of printers for arguments used only in vernac command
+
+- It should now use "declare_extra_vernac_genarg_pprule" rather than
+  "declare_extra_genarg_pprule", otherwise, a failure at runtime might
+  happen. An alternative is to register the corresponding argument as
+  a value, using "Geninterp.register_val0 wit None".
+
 ## Changes between Coq 8.6 and Coq 8.7
 
 ### Ocaml
-- 
cgit v1.2.3