diff options
Diffstat (limited to 'theories/Sorting')
| -rw-r--r-- | theories/Sorting/PermutEq.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v index 1e4673b641..e24380bffb 100644 --- a/theories/Sorting/PermutEq.v +++ b/theories/Sorting/PermutEq.v @@ -129,7 +129,7 @@ Lemma permut_nil : forall l, permutation l nil -> l = nil. Proof. intro l; destruct l as [ | e l ]; trivial. -assert (In e (e::l)) by red; auto. +assert (In e (e::l)) by (red; auto). intro Abs; generalize (permut_In_In _ Abs H). inversion 1. Qed. |