diff options
| author | Pierre-Marie Pédrot | 2017-08-02 17:31:13 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-02 17:51:23 +0200 |
| commit | d755c546a5c260232fd30971bd604b078d0afc18 (patch) | |
| tree | 91c6558476ef24bb8e0176cd34c5f4310193095d /doc | |
| parent | dbbefa2ed1f858c1a6de77672e3e1733ef4c28bf (diff) | |
Properly implementing the notation to easily access hypotheses.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/ltac2.md | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/doc/ltac2.md b/doc/ltac2.md index 12687e9aff..bf6d9eb583 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -470,8 +470,12 @@ as follows. constr:(fun x : nat => ltac2:(exact (hyp @x))) ``` -The `ltac2:(exact (hyp @x))` pattern is so common that we provide dedicated -Ltac2 and Coq term notations for it. +This pattern is so common that we provide dedicated Ltac2 and Coq term notations +for it. + +- `&x` as an Ltac2 expression expands to `hyp @x`. +- `&x` as an Coq constr expression expands to + `ltac2:(refine (fun () => hyp @x))`. #### Dynamic semantics |