diff options
| author | Hugo Herbelin | 2020-01-18 11:51:48 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-01-21 00:20:49 +0100 |
| commit | 64ea715e48b14ec8a793453b76db332e032d5cb0 (patch) | |
| tree | 2e2337b2817e1829087b9235723d4e4e4a7b7b3b /doc/sphinx | |
| parent | 26bf92e978eca1f405b302a2e02b1cadc4723b76 (diff) | |
Reference manual: Typos/English in chapter universe polymorphism.
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 7adb25cbd6..f9cc25959c 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -529,8 +529,8 @@ sections, except in the following ways: Polymorphic Universe i. Fail Constraint i = i. - This includes constraints implictly declared by commands such as - :cmd:`Variable`, which may as a such need to be used with universe + This includes constraints implicitly declared by commands such as + :cmd:`Variable`, which may need to be used with universe polymorphism activated (locally by attribute or globally by option): .. coqtop:: all |