diff options
Diffstat (limited to 'theories/Logic/ChoiceFacts.v')
| -rw-r--r-- | theories/Logic/ChoiceFacts.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index fb7898c6..1a32d518 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -344,7 +344,7 @@ Lemma rel_choice_and_proof_irrel_imp_guarded_rel_choice : RelationalChoice -> ProofIrrelevance -> GuardedRelationalChoice. Proof. intros rel_choice proof_irrel. - red in |- *; intros A B P R H. + red; intros A B P R H. destruct (rel_choice _ _ (fun (x:sigT P) (y:B) => R (projT1 x) y)) as (R',(HR'R,H0)). intros (x,HPx). destruct (H x HPx) as (y,HRxy). @@ -580,7 +580,7 @@ Lemma classical_denumerable_description_imp_fun_choice : (forall x y, decidable (R x y)) -> FunctionalChoice_on_rel R. Proof. intros A Descr. - red in |- *; intros R Rdec H. + red; intros R Rdec H. set (R':= fun x y => R x y /\ forall y', R x y' -> y <= y'). destruct (Descr R') as (f,Hf). intro x. |