From 6875b016b0a502b03296e5f97f26cf0f6699a7aa Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 25 Aug 2017 17:16:01 +0200
Subject: Do not return STRING scopes in the tuple produced by "seq" scopes.

---
 doc/ltac2.md | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/ltac2.md b/doc/ltac2.md
index 55780a7712..a645331e2d 100644
--- a/doc/ltac2.md
+++ b/doc/ltac2.md
@@ -615,8 +615,10 @@ The following scopes are built-in.
   + parses the string *s* as a keyword, if it is already a
     keyword, otherwise as an IDENT. Returns `()`.
 - seq(*scope₁*, ..., *scopeₙ*):
-  + parses *scope₁*, ..., *scopeₙ* in this order, and produces a n-tuple made
-    out of the parsed values in the same order. It is forbidden for the various
+  + parses *scope₁*, ..., *scopeₙ* in this order, and produces a tuple made
+    out of the parsed values in the same order. As an optimization, all
+    subscopes of the form STRING are left out of the returned tuple, instead
+    of returning a useless unit value. It is forbidden for the various
     subscopes to refer to the global entry using self of next.
 
 For now there is no way to declare new scopes from Ltac2 side, but this is
-- 
cgit v1.2.3