From d4cc73cb3b8f4ce9d3b8f2cd2e4377989bcbb465 Mon Sep 17 00:00:00 2001 From: Tanaka Akira Date: Thu, 31 Jan 2019 16:30:22 +0900 Subject: Don't line break at hyphen of compound words. --- doc/sphinx/language/cic.rst | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 18ddbe94cc..cd366e424b 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -989,8 +989,8 @@ the Type hierarchy. .. example:: It is well known that the existential quantifier can be encoded as an - inductive definition. The following declaration introduces the second- - order existential quantifier :math:`āˆƒ X.P(X)`. + inductive definition. The following declaration introduces the + second-order existential quantifier :math:`āˆƒ X.P(X)`. .. coqtop:: in @@ -1387,8 +1387,8 @@ of a computational object. In the same spirit, elimination on :math:`P` of type :math:`Iā†’\Type` cannot be allowed because it trivially implies the elimination on :math:`P` of type :math:`Iā†’ \Set` by cumulativity. It also implies that there are two proofs of the same -property which are provably different, contradicting the proof- -irrelevance property which is sometimes a useful axiom: +property which are provably different, contradicting the +proof-irrelevance property which is sometimes a useful axiom: .. example:: -- cgit v1.2.3