diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-07-26 15:06:52 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-07-26 15:06:52 +0200 |
| commit | 1cabc2981659f8f55b482b4392bcac9b9d200aa9 (patch) | |
| tree | 5c695c4f4bf95f51edaf6e23ea7ef8f736be9d41 /theories | |
| parent | 51d418636adf30bcf4e37a5b7b479a7d54dbedb2 (diff) | |
| parent | fa4e56987871c1b0a0b68e8f0864805e5f141ca9 (diff) | |
Merge PR #885: Removing a dummy parameter in some FMapPositive statements.
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/FSets/FMapPositive.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index b1c0fdaa2..3e7664929 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -654,19 +654,19 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Lemma xelements_bits_lt_1 : forall p p0 q m v, List.In (p0,v) (xelements m (append p (xO q))) -> E.bits_lt p0 p. - Proof. + Proof using. intros. generalize (xelements_complete _ _ _ _ H); clear H; intros. - revert p0 q m v H. + revert p0 H. induction p; destruct p0; simpl; intros; eauto; try discriminate. Qed. Lemma xelements_bits_lt_2 : forall p p0 q m v, List.In (p0,v) (xelements m (append p (xI q))) -> E.bits_lt p p0. - Proof. + Proof using. intros. generalize (xelements_complete _ _ _ _ H); clear H; intros. - revert p0 q m v H. + revert p0 H. induction p; destruct p0; simpl; intros; eauto; try discriminate. Qed. |