aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--doc/sphinx/language/cic.rst2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index f8c223d4da..b0bdd91ac6 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -186,7 +186,7 @@ object :math:`P~t` of type :math:`\Prop`, namely a proposition.
Furthermore :g:`forall x:nat, P x` will represent the type of functions
which associate to each natural number :math:`n` an object of type :math:`(P~n)` and
-consequently represent the type of proofs of the formula “:math:`∀ x. P(x`)”.
+consequently represent the type of proofs of the formula “:math:`∀ x. P(x)`”.
.. _Typing-rules: