From da4c116d650cc83171a8cd392307245cac826f73 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 30 Nov 2018 14:37:43 +0100
Subject: Accept argument names for extra arguments with "extra scopes"

The checks were unnecessarily restrictive (since names can be used for
documentation purposes), and the error message was a bit wrong (it
mentioned a restriction on the explicit status of arguments).
---
 CHANGES.md | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'CHANGES.md')

diff --git a/CHANGES.md b/CHANGES.md
index 8cb71f19ea..4fafb9a18a 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -88,6 +88,8 @@ Vernacular commands
 - The `Automatic Introduction` option has been removed and is now the
   default.
 
+- `Arguments` now accepts names for arguments provided with `extra_scopes`.
+
 Tools
 
 - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values:
-- 
cgit v1.2.3