diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-19 15:18:03 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-19 15:18:03 +0000 |
| commit | 508e8afd8538dd38afa4eaa0dd9c7e349e50e20d (patch) | |
| tree | a1b2f16de9eb4f35f49f6bf598331a7518588a7f /toplevel/libtypes.mli | |
| 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 'toplevel/libtypes.mli')
| -rw-r--r-- | toplevel/libtypes.mli | 26 |
1 files changed, 0 insertions, 26 deletions
diff --git a/toplevel/libtypes.mli b/toplevel/libtypes.mli deleted file mode 100644 index a4ce70e97..000000000 --- a/toplevel/libtypes.mli +++ /dev/null @@ -1,26 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Term - -(** Persistent library of all declared object, indexed by their types - (uses Dnets) *) - -(** results are the reference of the object, together with a context -(constr+evar) and a substitution under this context *) -type result = Globnames.global_reference * (constr*existential_key) * Termops.subst - -(** this is the reduction function used in the indexing process *) -val reduce : types -> types - -(** The different types of search available. - See term_dnet.mli for more explanations *) -val search_pattern : types -> result list -val search_concl : types -> result list -val search_head_concl : types -> result list -val search_eq_concl : constr -> types -> result list |