diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-07-08 16:57:15 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-07-08 17:04:48 +0200 |
| commit | 32dc4dc94c5677bc686a16a4a047f1750d0d8582 (patch) | |
| tree | dc1794d73f3ad4bad978e1c56c43f67bff6b347f /doc | |
| parent | 8b093fa1828eee800da2bc73de33ea8804175924 (diff) | |
Fix documentation of universes.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/Universes.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex index 341431114..018d73908 100644 --- a/doc/refman/Universes.tex +++ b/doc/refman/Universes.tex @@ -93,7 +93,7 @@ of monoids). \begin{coq_example*} Polymorphic Definition monoid_monoid : Monoid. - refine (@Build_Monoid Monoid unit_monoid _) ; admit. + refine (@Build_Monoid Monoid unit_monoid (fun x y => x)). Defined. \end{coq_example*} \begin{coq_example} |