diff options
| author | Pierre-Marie Pédrot | 2017-08-25 17:16:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-25 17:51:16 +0200 |
| commit | 6875b016b0a502b03296e5f97f26cf0f6699a7aa (patch) | |
| tree | 2802ed43b0a74af079acd05fd694a38938f94317 /doc | |
| parent | 47eb0278a3cdf93129b1742e314681d65bd6475a (diff) | |
Do not return STRING scopes in the tuple produced by "seq" scopes.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/ltac2.md | 6 |
1 files changed, 4 insertions, 2 deletions
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 |