Skip to content

Commit

Permalink
small typo in modules doc
Browse files Browse the repository at this point in the history
  • Loading branch information
Villetaneuse committed Jan 10, 2024
1 parent 50ca6d5 commit 94ea773
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion doc/sphinx/language/core/modules.rst
Original file line number Diff line number Diff line change
Expand Up @@ -941,7 +941,7 @@ with the logical name :n:`Top` and there is no associated file system path.

If :n:`@qualid` is the fully qualified name of an item, Coq
always interprets :n:`@qualid` as a reference to that item. If :n:`@qualid` is also a
partially qualified name for another item, then you must use provide a more-qualified
partially qualified name for another item, then you must provide a more-qualified
name to uniquely identify that other item. For example, if there are two
fully qualified items named `Foo.Bar` and `Coq.X.Foo.Bar`, then `Foo.Bar` refers
to the first item and `X.Foo.Bar` is the shortest name for referring to the second item.
Expand Down

0 comments on commit 94ea773

Please sign in to comment.