diff options
Diffstat (limited to 'doc/refman/RefMan-tacex.tex')
| -rw-r--r-- | doc/refman/RefMan-tacex.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex index 5703c73f0..668a68c9c 100644 --- a/doc/refman/RefMan-tacex.tex +++ b/doc/refman/RefMan-tacex.tex @@ -164,7 +164,7 @@ Notation " t --> t' " := (arrow t t') (at level 20, t' at next level). Inductive ctx : Type := | empty : ctx | snoc : ctx -> type -> ctx. -Notation " G , tau " := (snoc G tau) (at level 20, t at next level). +Notation " G , tau " := (snoc G tau) (at level 20, tau at next level). Fixpoint conc (G D : ctx) : ctx := match D with | empty => G |