diff options
| author | Tanaka Akira | 2019-01-31 17:42:31 +0900 |
|---|---|---|
| committer | Tanaka Akira | 2019-01-31 17:42:31 +0900 |
| commit | cdecb3f5bf0b0302cbfa0374053c97d81426e2c5 (patch) | |
| tree | 25c2e6b1b4c84fa9c078e752198048156179f966 | |
| parent | 000207cb082e016714ce21fd5e46baf281c41b9e (diff) | |
Insert a space before \kwend.
| -rw-r--r-- | doc/sphinx/language/cic.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 44928c3683..2083eb99a2 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1267,7 +1267,7 @@ The |Coq| term for this proof will be written: .. math:: - \Match~m~\with~(c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | … | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n \kwend + \Match~m~\with~(c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | … | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n~\kwend In this expression, if :math:`m` eventually happens to evaluate to :math:`(c_i~u_1 … u_{p_i})` then the expression will behave as specified in its :math:`i`-th branch |