From 52cdec561d76becf0d0120b73ea07510f3b2a9cd Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org> Date: Wed, 14 Sep 2016 16:24:52 +0200 Subject: [PATCH] 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 | 2 ++ theories/decidable.v | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/theories/base.v b/theories/base.v index 1d35448e..b7b02e23 100644 --- a/theories/base.v +++ b/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). diff --git a/theories/decidable.v b/theories/decidable.v index 545cafe2..8f45a83e 100644 --- a/theories/decidable.v +++ b/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). -- GitLab