aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Relations
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Relations')
-rw-r--r--theories/Relations/Relation_Operators.v10
1 files changed, 6 insertions, 4 deletions
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index 78857e3b8..abf23997d 100644
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -7,17 +7,19 @@
(************************************************************************)
(************************************************************************)
-(** * Bruno Barras, Cristina Cornes *)
+(** * Some operators on relations *)
+(************************************************************************)
+(** * Initial authors: Bruno Barras, Cristina Cornes *)
(** * *)
-(** * Some of these definitions were taken from : *)
+(** * Some of the initial definitions were taken from : *)
(** * Constructing Recursion Operators in Type Theory *)
(** * L. Paulson JSC (1986) 2, 325-355 *)
+(** * *)
+(** * Further extensions by Pierre Castéran *)
(************************************************************************)
Require Import Relation_Definitions.
-(** * Some operators to build relations *)
-
(** ** Transitive closure *)
Section Transitive_Closure.