From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 12 Nov 2007 16:41:30 +0000 (+0000)
Subject: ordered_sets are built with excedence
X-Git-Tag: 0.4.95@7852~17
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=abc2a8f11642390d930fbe81333f2f2b7467809d

ordered_sets are built with excedence
---

diff --git a/matita/dama/ordered_sets.ma b/matita/dama/ordered_sets.ma
index 5ae4f564a..3424edbb5 100644
--- a/matita/dama/ordered_sets.ma
+++ b/matita/dama/ordered_sets.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/ordered_sets/".
 
-include "ordered_sets.ma".
+include "excedence.ma".
 
 record is_porder_relation (C:Type) (le:C→C→Prop) (eq:C→C→Prop) : Type ≝ { 
   por_reflexive: reflexive ? le;