diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-02 10:27:45 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-02 10:27:45 +0000 |
| commit | 2de4563cb6192e638df4172c725ec8814e6eb112 (patch) | |
| tree | 424b7aad39c6a588d45d885f1f0178a20fa756e0 /theories/Sorting | |
| parent | 89d4f66beee6068a8ed227f8f03da153a43aabb0 (diff) | |
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
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 *) |