Bug fixed: the conversion was done with the wront argument (a sort of typo).

[helm.git] / matita / library / nat / ord.ma

diff --git a/matita/library/nat/ord.ma b/matita/library/nat/ord.ma
index e9353ba5b31af9903f2c8270025773c8b2c6e7fe..1ec8f68c5d1ad0c077b677bcd1a83767b70b1cee 100644 (file)
--- a/matita/library/nat/ord.ma
+++ b/matita/library/nat/ord.ma
@@ -17,6 +17,7 @@ set "baseuri" "cic:/matita/nat/ord".
 include "datatypes/constructors.ma".
 include "nat/exp.ma".
 include "nat/gcd.ma".
+include "nat/relevant_equations.ma". (* required by auto paramod *)
 
 (* this definition of log is based on pairs, with a remainder *)