From 2019b56bf43237167cc55512bbc13d82138abdb9 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Sun, 9 Sep 2012 22:24:34 +0000
Subject: 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
---
 lib/interface.mli | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

(limited to 'lib/interface.mli')

diff --git a/lib/interface.mli b/lib/interface.mli
index 07d82352b2..f8a382aefa 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 = {
-- 
cgit v1.2.3