From 4ac0580306ea9e45da1863316936d700969465ad Mon Sep 17 00:00:00 2001
From: filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 11 Apr 2001 12:41:41 +0000
Subject: documentation automatique de la bibliothèque standard
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1578 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Wellfounded/Lexicographic_Product.v | 4 ++--
 theories/Wellfounded/intro.tex               | 4 ++++
 2 files changed, 6 insertions(+), 2 deletions(-)
 create mode 100755 theories/Wellfounded/intro.tex

(limited to 'theories/Wellfounded')

diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v
index a51b876ab..419f545f5 100644
--- a/theories/Wellfounded/Lexicographic_Product.v
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -91,7 +91,7 @@ Section Wf_Symmetric_Product.
 
   Syntactic Definition Symprod := (symprod A B leA leB).
 
-(*
+(*i
   Local sig_prod:=
          [x:A*B]<{_:A&B}>Case x of [a:A][b:B](existS A [_:A]B a b) end.
 
@@ -108,7 +108,7 @@ Proof.
 
  (Apply right_lex;Auto with sets).
 Save.
-*)
+i*)
 
   Lemma Acc_symprod: (x:A)(Acc A leA x)->(y:B)(Acc B leB y)
                         ->(Acc (A*B) Symprod (x,y)).
diff --git a/theories/Wellfounded/intro.tex b/theories/Wellfounded/intro.tex
new file mode 100755
index 000000000..126071e28
--- /dev/null
+++ b/theories/Wellfounded/intro.tex
@@ -0,0 +1,4 @@
+\section{Well-founded relations}\label{Wellfounded}
+
+This library gives definitions and results about well-founded relations.
+
-- 
cgit v1.2.3