From 32dc4dc94c5677bc686a16a4a047f1750d0d8582 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 8 Jul 2015 16:57:15 +0200
Subject: Fix documentation of universes.

---
 doc/refman/Universes.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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}
-- 
cgit v1.2.3