From b03db7e43a67251406c4b27fa179f1d46c248906 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 21 Jun 2011 21:18:47 +0000 Subject: Follow-up concerning eqb / ltb / leb comparisons - All statement using reflect are made transparent. (Otherwise, since reflect isn't in Prop, extraction complains now about opaque Type definition). - remove two local Peqb_spec and Neqb_spec, now provided globally as Pos.eqb_spec and N.eqb_spec. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14232 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Bool/Bool.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'theories/Bool') diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 437ce5726..d5d11ceaa 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -791,7 +791,7 @@ Qed. Lemma iff_reflect : forall P b, (P<->b=true) -> reflect P b. Proof. destr_bool; intuition. -Qed. +Defined. (** It would be nice to join [reflect_iff] and [iff_reflect] in a unique [iff] statement, but this isn't allowed since @@ -802,7 +802,7 @@ Qed. Lemma reflect_dec : forall P b, reflect P b -> {P}+{~P}. Proof. destruct 1; auto. -Qed. +Defined. (** Reciprocally, from a decidability, we could state a [reflect] as soon as we have a [bool_of_sumbool]. *) -- cgit v1.2.3