Skip to content

Commit

Permalink
Merge PR coq#17793: Markup EQ as code.
Browse files Browse the repository at this point in the history
Reviewed-by: proux01
Co-authored-by: proux01 <[email protected]>
  • Loading branch information
coqbot-app[bot] and proux01 authored Jun 30, 2023
2 parents d7e6265 + ce84558 commit 12fe911
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion doc/sphinx/language/extensions/canonical.rst
Original file line number Diff line number Diff line change
Expand Up @@ -213,7 +213,7 @@ Note that in practice the user may want to declare ``EQ.obj`` as a
coercion, but we will not do that here.

The following line tests that, when we assume a type ``e`` that is in
theEQ class, we can relate two of its objects with ``==``.
the ``EQ`` class, we can relate two of its objects with ``==``.

.. coqtop:: all

Expand Down

0 comments on commit 12fe911

Please sign in to comment.