diff options
| author | Pierre-Marie Pédrot | 2017-08-24 14:58:46 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-24 15:41:15 +0200 |
| commit | 7d496e618f35a17b8432ac3c7205138f03c95fd2 (patch) | |
| tree | 747295c3a1364d96bc446abc491a53da3322729f /doc | |
| parent | 0232b0de849998d3394a4e6a2ab6232a75897610 (diff) | |
Introducing a quotation for global references.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/ltac2.md | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/ltac2.md b/doc/ltac2.md index b3596b2977..6c4912c8f3 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -437,6 +437,10 @@ The current implementation recognizes the following built-in quotations: holes at runtime (type `Init.constr` as well). - "pattern", which parses Coq patterns and produces a pattern used for term matching (type `Init.pattern`). +- "reference", which parses either a `QUALID` or `"&" IDENT`. Qualified names + are globalized at internalization into the corresponding global reference, + while `&id` is turned into `Std.VarRef id`. This produces at runtime a + `Std.reference`. The following syntactic sugar is provided for two common cases. - `@id` is the same as ident:(id) |