From 9c2662eecc398f38be3b6280a8f760cc439bc31c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 21 Jan 2016 01:43:10 +0100 Subject: Stronger invariants on the use of the introduction pattern (pat1,...,patn). The length of the pattern should now be exactly the number of assumptions and definitions introduced by the destruction or induction, including the induction hypotheses in case of an induction. Like for pattern-matching, the local definitions in the argument of the constructor can be skipped in which case a name is automatically created for these. --- theories/Sorting/Permutation.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Sorting') diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index fcb4e7876..ba7da256d 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -321,7 +321,7 @@ Proof. induction H; intros; try (injection Heqm; intros; subst; clear Heqm); 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 (); + apply IHPermutation1 in Heqm as [H1|H1]; apply IHPermutation2 in H1 as []; auto. Qed. -- cgit v1.2.3