From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 15 Sep 2005 17:39:01 +0000 (+0000)
Subject: "bool.ma" is now always included before "logic.ma", in order to speed up
X-Git-Tag: LAST_BEFORE_NEW~120
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=39eee3ee34bd22321d7b80c2685395345a0957e0;p=helm.git

"bool.ma" is now always included before "logic.ma", in order to speed up
parsing.
---

diff --git a/helm/matita/library/Z/compare.ma b/helm/matita/library/Z/compare.ma
index 551bfcf8a..4ae6dd2c4 100644
--- a/helm/matita/library/Z/compare.ma
+++ b/helm/matita/library/Z/compare.ma
@@ -14,10 +14,10 @@
 
 set "baseuri" "cic:/matita/Z/compare".
 
-include "Z/orders.ma".
-include "nat/compare.ma".
 include "datatypes/bool.ma".
 include "datatypes/compare.ma".
+include "Z/orders.ma".
+include "nat/compare.ma".
 
 (* boolean equality *)
 definition eqZb : Z \to Z \to bool \def
diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma
index 194b38d84..852cd7b65 100644
--- a/helm/matita/library/nat/compare.ma
+++ b/helm/matita/library/nat/compare.ma
@@ -14,9 +14,9 @@
 
 set "baseuri" "cic:/matita/nat/compare".
 
-include "nat/orders.ma".
 include "datatypes/bool.ma".
 include "datatypes/compare.ma".
+include "nat/orders.ma".
 
 let rec eqb n m \def 
 match n with 
diff --git a/helm/matita/library/nat/minimization.ma b/helm/matita/library/nat/minimization.ma
index 5eaa02cc3..bb3475150 100644
--- a/helm/matita/library/nat/minimization.ma
+++ b/helm/matita/library/nat/minimization.ma
@@ -15,7 +15,6 @@
 set "baseuri" "cic:/matita/nat/minimization".
 
 include "nat/minus.ma".
-include "datatypes/bool.ma".
 
 let rec max i f \def
   match (f i) with 
diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma
index c85bb25c2..f8ff252ae 100644
--- a/helm/matita/library/nat/nat.ma
+++ b/helm/matita/library/nat/nat.ma
@@ -14,9 +14,9 @@
 
 set "baseuri" "cic:/matita/nat/nat".
 
+include "datatypes/bool.ma".
 include "logic/equality.ma".
 include "logic/connectives.ma".
-include "datatypes/bool.ma".
 include "higher_order_defs/functions.ma".
 
 inductive nat : Set \def