From 2de4563cb6192e638df4172c725ec8814e6eb112 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 2 Jul 2010 10:27:45 +0000 Subject: Sorting library: export as hints only lemmas that obviously simplify the size of the problem to solve. This is still more powerful than what 8.2 provided since no hints were exported yet when Permutation was in List.v in 8.2. Whether no hints should be exported at all, and whether hints should be exported in a specific database or not is unclear. At least, the contribs apparently supported the extra added power of auto introduced in r12585 (date of the revision of the Sorting library), so let's continue with it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13231 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Sorting/Permutation.v | 13 +++++++++---- theories/Sorting/Sorted.v | 4 ++-- 2 files changed, 11 insertions(+), 6 deletions(-) (limited to 'theories/Sorting') 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 *) -- cgit v1.2.3