diff options
| author | ppedrot | 2013-03-19 15:18:03 +0000 |
|---|---|---|
| committer | ppedrot | 2013-03-19 15:18:03 +0000 |
| commit | 508e8afd8538dd38afa4eaa0dd9c7e349e50e20d (patch) | |
| tree | a1b2f16de9eb4f35f49f6bf598331a7518588a7f /ide/wg_MessageView.ml | |
| parent | 906b063b798e6c0787fd8f514b9d7f1f8eef9cf8 (diff) | |
Removing the module Libtypes and unifying the Search[Pattern|Rewrite]?
mechanism with the SearchAbout one. Searches may be slower, but this
is unlikely to be noticed. In addition, according to Hugo, the
Libtype summary was imposing a noticeable time penalty without
any real advantage.
Now Search and SearchPattern are the same. The documentation was not
really clear about the difference between both, except that Search
was restricted to closed terms. This is an artificial restriction by
now.
Fixing #2815 btw.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16320 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/wg_MessageView.ml')
0 files changed, 0 insertions, 0 deletions