diff options
Diffstat (limited to 'theories/Sorting')
-rw-r--r-- | theories/Sorting/Permutation.v | 13 | ||||
-rw-r--r-- | theories/Sorting/Sorted.v | 4 |
2 files changed, 11 insertions, 6 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). diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v index 931e29bf8..5cc73f3be 100644 --- a/theories/Sorting/Sorted.v +++ b/theories/Sorting/Sorted.v @@ -133,8 +133,8 @@ Section defs. End defs. -Hint Constructors HdRel: sorting. -Hint Constructors Sorted: sorting. +Hint Constructors HdRel. +Hint Constructors Sorted. (* begin hide *) (* Compatibility with deprecated file Sorting.v *) |