diff options
| -rw-r--r-- | doc/sphinx/language/cic.rst | 8 |
1 files 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:: |