diff options
| author | Hugo Herbelin | 2019-05-23 17:27:08 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-05-25 15:36:59 +0200 |
| commit | 71110a218f69a69010adde2f296e4022ef94b755 (patch) | |
| tree | db5d944a60f3d211191f10d3caa3b716af80d6ee /theories/Sorting | |
| parent | 7050ceaa09a29c3f50620a8d3f8439c3d69a10d0 (diff) | |
Modifying theories to preferably use the "[= ]" syntax, and,
sometimes, to use "intros [= ...]" rather than things like "intros H;
injection H as [= ...]".
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
Diffstat (limited to 'theories/Sorting')
| -rw-r--r-- | theories/Sorting/Permutation.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index f5bc9eee4e..170c221a45 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -304,7 +304,7 @@ Qed. Lemma Permutation_length_1_inv: forall a l, Permutation [a] l -> l = [a]. Proof. intros a l H; remember [a] as m in H. - induction H; try (injection Heqm as -> ->); + induction H; try (injection Heqm as [= -> ->]); discriminate || auto. apply Permutation_nil in H as ->; trivial. Qed. @@ -312,7 +312,7 @@ Qed. Lemma Permutation_length_1: forall a b, Permutation [a] [b] -> a = b. Proof. intros a b H. - apply Permutation_length_1_inv in H; injection H as ->; trivial. + apply Permutation_length_1_inv in H; injection H as [= ->]; trivial. Qed. Lemma Permutation_length_2_inv : @@ -320,7 +320,7 @@ Lemma Permutation_length_2_inv : Proof. intros a1 a2 l H; remember [a1;a2] as m in H. revert a1 a2 Heqm. - induction H; intros; try (injection Heqm as ? ?; subst); + induction H; intros; try (injection Heqm as [= ? ?]; subst); discriminate || (try tauto). apply Permutation_length_1_inv in H as ->; left; auto. apply IHPermutation1 in Heqm as [H1|H1]; apply IHPermutation2 in H1 as []; @@ -332,7 +332,7 @@ Lemma Permutation_length_2 : a1 = b1 /\ a2 = b2 \/ a1 = b2 /\ a2 = b1. Proof. intros a1 b1 a2 b2 H. - apply Permutation_length_2_inv in H as [H|H]; injection H as -> ->; auto. + apply Permutation_length_2_inv in H as [H|H]; injection H as [= -> ->]; auto. Qed. Lemma NoDup_Permutation l l' : NoDup l -> NoDup l' -> |