diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-06-29 17:35:24 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-06-29 17:35:24 +0200 |
| commit | 9e981eca272e571924b535de47263e33658648be (patch) | |
| tree | cf475c8a3ee31f6f3a5122e5b6d71e1fa2456de6 | |
| parent | 9446c06675ec0b20dcdf871337ce3f18b76ba516 (diff) | |
Better phrasing.
| -rw-r--r-- | doc/tutorial/Tutorial.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex index 9e085bbea..3a91664db 100644 --- a/doc/tutorial/Tutorial.tex +++ b/doc/tutorial/Tutorial.tex @@ -1550,7 +1550,7 @@ SearchHead le. The \verb:Search: commands also allows finding the theorems containing a given pattern, where \verb:_: can be used in -place of an arbitrary term. Note in passing that \Coq{} +place of an arbitrary term. As shown in this example, \Coq{} provides usual infix notations for arithmetic operators. \begin{coq_example} |