diff options
| author | Hugo Herbelin | 2017-08-26 09:40:31 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-08-26 09:40:31 +0200 |
| commit | bec2a0ad6eb60d33b5e3ab613d108f456df42a49 (patch) | |
| tree | 61404a001fb389ea8709a7ce229db89e609fde21 | |
| parent | 126dc656963a7feb589b2a3574f0c55ad84d5f69 (diff) | |
Typos
| -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 51e3ab664d..5b1776b64f 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -488,7 +488,7 @@ Ltac2 Definition myconstr () := constr:(nat -> 0). ``` Term antiquotations are type-checked in the enclosing Ltac2 typing context -of the corresponding term expression. For instance, the following with +of the corresponding term expression. For instance, the following will type-check. ``` @@ -523,7 +523,7 @@ 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 +- `&x` as a Coq constr expression expands to `ltac2:(refine (fun () => hyp @x))`. #### Dynamic semantics @@ -538,7 +538,7 @@ under focus, with the hypotheses coming from the current environment extended with the bound variables of the term, and the resulting term is fed into the quoted term. -Relative orders of evaluation of antiquotations and quoted term is not +Relative orders of evaluation of antiquotations and quoted term are not specified. For instance, in the following example, `tac` will be evaluated in a context |