-(* The point is that == expects in input a pair of objects object whose type
-must be the carrier of a DeqSet; bool is indeed the carrier of DeqBool, but the
-type inference system has no knowledge of it (it is an information that has been
-supplied by the user, and stored somewhere in the library). More explicitly, the
-type inference inference system, would face an unification problem consisting to
-unify bool against the carrier of something (a metavaribale) and it has no way to
-synthetize the answer. To solve this kind of situations, matita provides a
-mechanism to hint the system the expected solution. A unification hint is a kind of
-rule, whose rhd is the unification problem, containing some metavariables X1, ...,
-Xn, and whose left hand side is the solution suggested to the system, in the form
-of equations Xi=Mi. The hint is accepted by the system if and only the solution is
-correct, that is, if it is a unifier for the given problem.
+(* The point is that == expects in input a pair of objects whose type must be the
+carrier of a DeqSet; bool is indeed the carrier of DeqBool, but the type inference
+system has no knowledge of it (it is an information that has been supplied by the
+user, and stored somewhere in the library). More explicitly, the type inference
+inference system, would face an unification problem consisting to unify bool
+against the carrier of something (a metavaribale) and it has no way to synthetize
+the answer. To solve this kind of situations, matita provides a mechanism to hint
+the system the expected solution. A unification hint is a kind of rule, whose rhd
+is the unification problem, containing some metavariables X1, ..., Xn, and whose
+left hand side is the solution suggested to the system, in the form of equations
+Xi=Mi. The hint is accepted by the system if and only the solution is correct, that
+is, if it is a unifier for the given problem.