From fdb79e2cd4bc712d916deacfcba33136683b37b2 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. --- prelude/base.v | 2 ++ prelude/decidable.v | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/prelude/base.v b/prelude/base.v index 1d35448e8..b7b02e230 100644 --- a/prelude/base.v +++ b/prelude/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/prelude/decidable.v b/prelude/decidable.v index 76ec22103..7b6431a6f 100644 --- a/prelude/decidable.v +++ b/prelude/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