mod change (-x)

[helm.git] / helm / software / matita / contribs / ng_assembly2 / num / comp_num.ma

diff --git a/helm/software/matita/contribs/ng_assembly2/num/comp_num.ma b/helm/software/matita/contribs/ng_assembly2/num/comp_num.ma
old mode 100755 (executable)
new mode 100644 (file)
index a062a56..e9c15dd
--- a/helm/software/matita/contribs/ng_assembly2/num/comp_num.ma
+++ b/helm/software/matita/contribs/ng_assembly2/num/comp_num.ma
@@ -216,7 +216,7 @@ nlemma cn_is_comparable : comparable → comparable.
 nqed.
 
 nlemma cn_is_comparable_ext : comparable_ext → comparable_ext.
- #T; nelim T; #c; 
+ #T; nelim T; #c;
  #ltc; #lec; #gtc; #gec; #andc; #orc; #xorc;
  #getMSBc; #setMSBc; #clrMSBc; #getLSBc; #setLSBc; #clrLSBc;
  #rcrc; #shrc; #rorc; #rclc; #shlc; #rolc; #notc;
@@ -337,12 +337,6 @@ nlemma cn_is_comparable_ext : comparable_ext → comparable_ext.
   ##]
 nqed.
 
-unification hint 0 ≔ S: comparable;
-         T ≟ (carr S),
-         X ≟ (cn_is_comparable S)
- (*********************************************) ⊢
-         carr X ≡ comp_num T.
-
 ndefinition zeroc ≝ λx:comparable_ext.zeroc (comp_base x).
 ndefinition forallc ≝ λx:comparable_ext.forallc (comp_base x).
 ndefinition eqc ≝ λx:comparable_ext.eqc (comp_base x).
@@ -352,3 +346,10 @@ ndefinition neqc_to_neq ≝ λx:comparable_ext.neqc_to_neq (comp_base x).
 ndefinition neq_to_neqc ≝ λx:comparable_ext.neq_to_neqc (comp_base x).
 ndefinition decidable_c ≝ λx:comparable_ext.decidable_c (comp_base x).
 ndefinition symmetric_eqc ≝ λx:comparable_ext.symmetric_eqc (comp_base x).
+
+
+unification hint 0 ≔ S: comparable;
+         T ≟ (carr S),
+         X ≟ (cn_is_comparable S)
+ (*********************************************) ⊢
+         carr X ≡ comp_num T.