"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 551bfcf8a4333854e8af5ef99a7acca21ab2ae1e..4ae6dd2c41e636921d45a8b040432baeb7c0237c 100644 (file)
--- 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 194b38d84f255e3924a3273919f01bb96d320ca5..852cd7b6551f44091425aebcbac65ae7d314c6fb 100644 (file)
--- 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 5eaa02cc36922378f9dbca5755aa22651bbbcb7b..bb3475150092077bed0f14ff915dcf0fc0b531e8 100644 (file)
--- 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 c85bb25c2c04faf4ace9c21e65527f89d6536331..f8ff252aeae6c4e11ae88c484eac2908fd507d33 100644 (file)
--- 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