aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Relations/Relation_Operators.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Relations/Relation_Operators.v')
-rwxr-xr-xtheories/Relations/Relation_Operators.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index a5c81e2e3..7b07ac0db 100755
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -20,7 +20,7 @@ Require Relation_Definitions.
Require PolyList.
Require PolyListSyntax.
-(* Some operators to build relations *)
+(** Some operators to build relations *)
Section Transitive_Closure.
Variable A: Set.