From d51d98682fcff981a1e6b95574c25fc7edf97b3f Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 2 Jun 2013 21:42:11 +0000 Subject: Making the behavior of "injection ... as ..." more natural: - hypotheses are introduced in the left-to-right order - intropatterns have to match the number of generated hypotheses, and, if less, new introduction names are automatically generated - clearing the hypothesis on which injection is applied, if any. However, this is a source of incompatibilities (for a variant of injection that is hopefully not used a lot). Compatibility can be restored by "Unset Injection L2R Pattern Order". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16556 85f007b7-540e-0410-9357-904b9bb8a0f7 --- 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 65bf17ef0..cf9f8ee42 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -313,7 +313,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 -> ->; clear Heqm); + induction H; try (injection Heqm as -> ->); discriminate || auto. apply Permutation_nil in H as ->; trivial. Qed. -- cgit v1.2.3