diff options
Diffstat (limited to 'theories/Init/Tactics.v')
| -rw-r--r-- | theories/Init/Tactics.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index b13206db94..6b4551318b 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -203,7 +203,7 @@ Set Implicit Arguments. Lemma decide_left : forall (C:Prop) (decide:{C}+{~C}), C -> forall P:{C}+{~C}->Prop, (forall H:C, P (left _ H)) -> P decide. Proof. - intros; destruct decide. + intros C decide H P H0; destruct decide. - apply H0. - contradiction. Qed. @@ -211,7 +211,7 @@ Qed. Lemma decide_right : forall (C:Prop) (decide:{C}+{~C}), ~C -> forall P:{C}+{~C}->Prop, (forall H:~C, P (right _ H)) -> P decide. Proof. - intros; destruct decide. + intros C decide H P H0; destruct decide. - contradiction. - apply H0. Qed. |