diff options
| -rw-r--r-- | doc/ltac2.md | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/ltac2.md b/doc/ltac2.md index fee19e5df0..7a3b2181f8 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -467,11 +467,11 @@ Rather, the tactic writer has to resort to the **dynamic** goal environment, and must write instead explicitly that she is accessing a hypothesis, typically as follows. ``` -constr:(fun x : nat => ltac2:(hyp @x)) +constr:(fun x : nat => ltac2:(exact (hyp @x))) ``` -The `ltac2:(hyp @x)` pattern is so common that we provide a dedicated Coq -term notation for it. +The `ltac2:(exact (hyp @x))` pattern is so common that we provide dedicated +Ltac2 and Coq term notations for it. #### Dynamic semantics |