diff options
| author | Théo Zimmermann | 2020-01-21 10:03:03 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-01-21 10:03:03 +0100 |
| commit | f93782dbbb2e61e6664a09b3ae7981223e57f9d3 (patch) | |
| tree | 494a4581396aa00a67ab63c3564603c268e96a65 /doc/sphinx | |
| parent | 4d12b00277aa1bfde14ba459363a5e9d38d4aeac (diff) | |
| parent | 61afb01b721d12068ade37f5c809319668e3573e (diff) | |
Merge PR #11425: Miscellaneous typos
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: jfehrle
Reviewed-by: ppedrot
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 |