snapshot for CSC

[helm.git] / helm / software / matita / nlibrary / logic / cprop.ma

diff --git a/helm/software/matita/nlibrary/logic/cprop.ma b/helm/software/matita/nlibrary/logic/cprop.ma
index d006599ed93b49ffdb42ab46f8d1edbccd9b993a..339f733567bb48da0a23626800a98a2bfe91e65c 100644 (file)
--- a/helm/software/matita/nlibrary/logic/cprop.ma
+++ b/helm/software/matita/nlibrary/logic/cprop.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "hints_declaration.ma".
 include "sets/setoids1.ma".
 
 ndefinition CPROP: setoid1.
@@ -25,7 +26,8 @@ ndefinition CPROP: setoid1.
         [ napply (H3 (H1 w)) | napply (H2 (H4 w))]##]##]
 nqed.
 
-unification hint 0 ((λx,y.True) (carr1 CPROP) CProp[0]).
+alias symbol "hint_decl" = "hint_decl_CProp2".
+unification hint 0 ≔ ⊢ CProp[0] ≡ carr1 CPROP.
 
 (*ndefinition CProp0_of_CPROP: carr1 CPROP → CProp[0] ≝ λx.x.
 ncoercion CProp0_of_CPROP : ∀x: carr1 CPROP. CProp[0] ≝ CProp0_of_CPROP