Added alias instance=1 to avoid interaction with the user.

[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 e874eb8ffe6487fd9cd5bc7489c3ed375030ffc3..45afabe59ad9555e55f863c8b9e3a584c5ac5963 100644 (file)
--- 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
 (* ---------------------------------------- *) ⊢