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/Sorted.v | |
| 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/Sorted.v')
| -rw-r--r-- | theories/Sorting/Sorted.v | 4 |
1 files changed, 2 insertions, 2 deletions
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 *) |