From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 theories/Relations/Relation_Operators.v | 18 ++++++++++++++++--
 1 file changed, 16 insertions(+), 2 deletions(-)

(limited to 'theories/Relations/Relation_Operators.v')

diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index 701bc073..4e52017e 100644
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -46,6 +46,20 @@ Section Transitive_Closure.
 
 End Transitive_Closure.
 
+(** ** Reflexive closure *)
+
+Section Reflexive_Closure.
+  Variable A : Type.
+  Variable R : relation A.
+
+  (** Definition by direct transitive closure *)
+
+  Inductive clos_refl (x: A) : A -> Prop :=
+    | r_step (y:A) : R x y -> clos_refl x y
+    | r_refl : clos_refl x x.
+
+End Reflexive_Closure.
+
 (** ** Reflexive-transitive closure *)
 
 Section Reflexive_Transitive_Closure.
@@ -204,7 +218,7 @@ Section Lexicographic_Exponentiation.
     | d_nil : Desc Nil
     | d_one (x:A) : Desc (x :: Nil)
     | d_conc (x y:A) (l:List) :
-        leA x y -> Desc (l ++ y :: Nil) -> Desc ((l ++ y :: Nil) ++ x :: Nil).
+        clos_refl A leA x y -> Desc (l ++ y :: Nil) -> Desc ((l ++ y :: Nil) ++ x :: Nil).
 
   Definition Pow : Set := sig Desc.
 
-- 
cgit v1.2.3