diff options
author | Stephane Glondu <steph@glondu.net> | 2012-12-29 10:57:43 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-12-29 10:57:43 +0100 |
commit | bf12eb93f3f6a6a824a10878878fadd59745aae0 (patch) | |
tree | 279f64f4b7e4804415ab5731cc7aaa8a4fcfe074 /toplevel/interface.mli | |
parent | e0d682ec25282a348d35c5b169abafec48555690 (diff) |
Imported Upstream version 8.4pl1dfsgupstream/8.4pl1dfsg
Diffstat (limited to 'toplevel/interface.mli')
-rw-r--r-- | toplevel/interface.mli | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/toplevel/interface.mli b/toplevel/interface.mli index 39fb2a0e..7b4312a3 100644 --- a/toplevel/interface.mli +++ b/toplevel/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 = { |