Merge branch 'matita-lablgtk3' of ssh://matita.cs.unibo.it:/srv/git/helm into matita...

[helm.git] / matita / matita / lib / basics / deqsets.ma

diff --git a/matita/matita/lib/basics/deqsets.ma b/matita/matita/lib/basics/deqsets.ma
index fcc89f3127007036a20a4b09e62b9b72d3bd0570..c17db5dc0cb4b1e899ae76533a686ad5322fb450 100644 (file)
--- a/matita/matita/lib/basics/deqsets.ma
+++ b/matita/matita/lib/basics/deqsets.ma
@@ -14,11 +14,12 @@ include "basics/bool.ma".
 
 (****** DeqSet: a set with a decidbale equality ******)
 
-record DeqSet : Type[1] ≝ { carr :> Type[0];
+record DeqSet : Type[1] ≝ { 
+   carr :> Type[0];
    eqb: carr → carr → bool;
    eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)
 }.
-
+    
 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
 interpretation "eqb" 'eqb a b = (eqb ? a b).
 
@@ -207,7 +208,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 +220,4 @@ unification hint  0 ≔ T,P,p1,p2;
     X ≟ DeqSig T P
 (* ---------------------------------------- *) ⊢ 
     eq_sigma T P p1 p2 ≡ eqb X p1 p2.
-
+*)