X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Fdeqsets.ma;h=45afabe59ad9555e55f863c8b9e3a584c5ac5963;hb=f0d422b660e11886ec4f9a823da795050f07e07f;hp=e874eb8ffe6487fd9cd5bc7489c3ed375030ffc3;hpb=08a53e81b883cc19ddec52a662e9c171656ec364;p=helm.git

diff --git a/matita/matita/lib/basics/deqsets.ma b/matita/matita/lib/basics/deqsets.ma
index e874eb8ff..45afabe59 100644
--- a/matita/matita/lib/basics/deqsets.ma
+++ b/matita/matita/lib/basics/deqsets.ma
@@ -61,6 +61,7 @@ qed.
 
 definition DeqBool ≝ mk_DeqSet bool beqb beqb_true.
 
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
 unification hint  0 ≔ ; 
     X ≟ mk_DeqSet bool beqb beqb_true
 (* ---------------------------------------- *) ⊢