aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--doc/sphinx/language/gallina-extensions.rst2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 4ca20ce313..a8d6d2632b 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2081,7 +2081,7 @@ in :ref:`canonicalstructures`; here only a simple example is given.
canonical structure. For each of them, the canonical structure of
which it is a projection is indicated. If constants are given as
its arguments, only the unification rules that involve or are
- synthesized from given constants will be shown.
+ synthesized from simultaneously all given constants will be shown.
.. example::