From a3281b10a5ec5721eac591ef5cfe273238d2e377 Mon Sep 17 00:00:00 2001
From: marche
Date: Tue, 16 Dec 2003 16:07:54 +0000
Subject: coqide menus on golas

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8403 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-lib.tex | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'doc/RefMan-lib.tex')

diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex
index be1be5ca05..38ab55515f 100755
--- a/doc/RefMan-lib.tex
+++ b/doc/RefMan-lib.tex
@@ -386,7 +386,8 @@ provided.
 
 \begin{coq_example*}
 Inductive sig (A:Set) (P:A -> Prop) : Set := exist (x:A) (_:P x).
-Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := exist2 : (x:A) (_:P x) (_:Q x).
+Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := 
+  exist2 : (x:A) (_:P x) (_:Q x).
 \end{coq_example*}
 
 A ``strong (dependent) sum'' \verb+{x:A & (P x)}+ may be also defined,
-- 
cgit v1.2.3