diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-09 22:24:34 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-09 22:24:34 +0000 |
| commit | 2019b56bf43237167cc55512bbc13d82138abdb9 (patch) | |
| tree | 7f35d5154b47f39d87fcdc4f2faa87a1e03280bc /lib/interface.mli | |
| parent | 56dc4da6ddafe885f6be0dcb300a6449541eab35 (diff) | |
When asked for a SearchAbout request, Coq now returns a more precise
name, that is, a pair of a smart qualified name and the missing
prefix needed to recover the full path.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15787 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/interface.mli')
| -rw-r--r-- | lib/interface.mli | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/lib/interface.mli b/lib/interface.mli index 07d82352b..f8a382aef 100644 --- a/lib/interface.mli +++ b/lib/interface.mli @@ -86,10 +86,14 @@ type search_constraint = the flag should be negated. *) type search_flags = (search_constraint * bool) list -type search_answer = { - search_answer_full_path : string list; - search_answer_base_name : string; - search_answer_type : string; +(** A named object in Coq. [coq_object_qualid] is the shortest path defined for + the user. [coq_object_prefix] is the missing part to recover the fully + qualified name, i.e [fully_qualified = coq_object_prefix + coq_object_qualid]. + [coq_object_object] is the actual content of the object. *) +type 'a coq_object = { + coq_object_prefix : string list; + coq_object_qualid : string list; + coq_object_object : 'a; } type coq_info = { |