From d857c99c6c985eb36ce8a4b2667dc0b5ccca115c Mon Sep 17 00:00:00 2001 From: coq Date: Fri, 20 Apr 2001 16:00:43 +0000 Subject: Library doc adjustments (until page 140) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1655 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Relations/Newman.v | 8 ++++---- theories/Relations/Relation_Operators.v | 2 +- theories/Relations/Rstar.v | 4 ++-- 3 files changed, 7 insertions(+), 7 deletions(-) (limited to 'theories/Relations') diff --git a/theories/Relations/Newman.v b/theories/Relations/Newman.v index 966a755c5..e7829b00e 100755 --- a/theories/Relations/Newman.v +++ b/theories/Relations/Newman.v @@ -85,14 +85,14 @@ Proof (* We draw the diagram ! *) Theorem caseRxy : (coherence y z). Proof (Rstar_Rstar' x z h2 ([v:A][w:A](coherence y w)) - (coherence_sym x y (Rstar_coherence x y h1)) (* case x=z *) - Diagram). (* case x->v->*z *) + (coherence_sym x y (Rstar_coherence x y h1)) (*i case x=z i*) + Diagram). (*i case x->v->*z i*) End Newman_. Theorem Ind_proof : (coherence y z). Proof (Rstar_Rstar' x y h1 ([u:A][v:A](coherence v z)) - (Rstar_coherence x z h2) (* case x=y*) - caseRxy). (* case x->u->*z *) + (Rstar_coherence x z h2) (*i case x=y i*) + caseRxy). (*i case x->u->*z i*) End Induct. Theorem Newman : (x:A)(confluence x). diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v index a5ee00157..a5c81e2e3 100755 --- a/theories/Relations/Relation_Operators.v +++ b/theories/Relations/Relation_Operators.v @@ -9,7 +9,7 @@ (*i $Id$ i*) (****************************************************************************) -(* Bruno Barras Cristina Cornes *) +(* Bruno Barras, Cristina Cornes *) (* *) (* Some of these definitons were taken from : *) (* Constructing Recursion Operators in Type Theory *) diff --git a/theories/Relations/Rstar.v b/theories/Relations/Rstar.v index 0df3af6b4..a0aaed9ad 100755 --- a/theories/Relations/Rstar.v +++ b/theories/Relations/Rstar.v @@ -10,8 +10,8 @@ (* Properties of a binary relation R on type A *) - Parameter A : Type. - Parameter R : A->A->Prop. +Parameter A : Type. +Parameter R : A->A->Prop. (* Definition of the reflexive-transitive closure R* of R *) (* Smallest reflexive P containing R o P *) -- cgit v1.2.3