From d286c3601e24afe0a681d092cbd880773872b980 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 15 Sep 2020 21:24:39 +0200
Subject: Fixes #9716, #13004: don't drop the qualifier of quotations at
 printing time.

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

(limited to 'dev/doc/changes.md')

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index ae4c6328b5..7d2100515d 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,5 +1,9 @@
 ## Changes between Coq 8.12 and Coq 8.13
 
+- Tactic language: TacGeneric now takes an argument to tell if it
+  comes from a notation. Use `None` if not and `Some foo` to tell to
+  print such TacGeneric surrounded with `foo:( )`.
+
 ## Changes between Coq 8.11 and Coq 8.12
 
 ### Code formatting
-- 
cgit v1.2.3