X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Fdeqsets.ma;h=fb6ad5be4fe3f11a678f11e62cea79b14ba8cfb6;hb=95ea23408caad83226b7a9206f3e020accf3f9ce;hp=fcc89f3127007036a20a4b09e62b9b72d3bd0570;hpb=347a03a55e60c5a4682e0133454ff87ce21a4e8c;p=helm.git

diff --git a/matita/matita/lib/basics/deqsets.ma b/matita/matita/lib/basics/deqsets.ma
index fcc89f312..fb6ad5be4 100644
--- a/matita/matita/lib/basics/deqsets.ma
+++ b/matita/matita/lib/basics/deqsets.ma
@@ -207,7 +207,8 @@ qed.
 
 definition DeqSig ≝ λA:DeqSet.λP:A→Prop.
   mk_DeqSet (Σx:A.P x) (eq_sigma A P) (eq_sigma_true A P).
-  
+
+(*
 unification hint  0 ≔ C,P; 
     T ≟ carr C,
     X ≟ DeqSig C P
@@ -218,4 +219,4 @@ unification hint  0 ≔ T,P,p1,p2;
     X ≟ DeqSig T P
 (* ---------------------------------------- *) ⊢ 
     eq_sigma T P p1 p2 ≡ eqb X p1 p2.
-
+*)