diff options
| -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 3414311148..018d73908b 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} |