Make Is_true a typeclass.

This makes the typeclass mechanism able to use instances like [Is_true X -> Blah], where X reduces to X.

theories/base.v

@@ -374,6 +374,8 @@ Notation zip := (zip_with pair).
 Coercion Is_true : bool >-> Sortclass.
 Hint Unfold Is_true.
 Hint Immediate Is_true_eq_left.
+Existing Class Is_true.
+Instance true_Is_true : Is_true true := I.
 Hint Resolve orb_prop_intro andb_prop_intro.
 Notation "(&&)" := andb (only parsing).
 Notation "(||)" := orb (only parsing).

theories/decidable.v

@@ -146,7 +146,7 @@ Proof. apply dsig_eq; reflexivity. Qed.
 Instance True_dec: Decision True := left I.
 Instance False_dec: Decision False := right (False_rect False).
 Instance Is_true_dec b : Decision (Is_true b).
-Proof. destruct b; apply _. Defined.
+Proof. destruct b; simpl; apply _. Defined.
 
 Section prop_dec.
   Context `(P_dec : Decision P) `(Q_dec : Decision Q).