diff options
Diffstat (limited to 'theories/Sorting/Permutation.v')
| -rw-r--r-- | theories/Sorting/Permutation.v | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index e861b9ce7..973003a0d 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -30,7 +30,7 @@ Inductive Permutation : list A -> list A -> Prop := | perm_swap x y l : Permutation (y::x::l) (x::y::l) | perm_trans l l' l'' : Permutation l l' -> Permutation l' l'' -> Permutation l l''. -Hint Constructors Permutation. +Local Hint Constructors Permutation. (** Some facts about [Permutation] *) @@ -67,8 +67,13 @@ Qed. End Permutation. -Hint Constructors Permutation. -Hint Resolve Permutation_refl Permutation_sym Permutation_trans. +Hint Resolve Permutation_refl perm_nil perm_skip. + +(* These hints do not reduce the size of the problem to solve and they + must be used with care to avoid combinatoric explosions *) + +Local Hint Resolve perm_swap perm_trans. +Local Hint Resolve Permutation_sym Permutation_trans. (* This provides reflexivity, symmetry and transitivity and rewriting on morphims to come *) @@ -159,7 +164,7 @@ Proof. apply perm_swap; auto. apply perm_skip; auto. Qed. -Hint Resolve Permutation_cons_app. +Local Hint Resolve Permutation_cons_app. Theorem Permutation_middle : forall (l1 l2:list A) a, Permutation (a :: l1 ++ l2) (l1 ++ a :: l2). |