1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Cdglobals
type loc = int
type entry_type =
| Library
| Module
| Definition
| Inductive
| Constructor
| Lemma
| Record
| Projection
| Instance
| Class
| Method
| Variable
| Axiom
| TacticDefinition
| Abbreviation
| Notation
| Section
val type_name : entry_type -> string
type index_entry =
| Def of string * entry_type
| Ref of coq_module * string * entry_type
(* Find what symbol coqtop said is located at loc in the source file *)
val find : coq_module -> loc -> index_entry
(* Find what data is referred to by some string in some coq module *)
val find_string : coq_module -> string -> index_entry
val add_module : coq_module -> unit
type module_kind = Local | External of coq_module | Unknown
val find_module : coq_module -> module_kind
val init_coqlib_library : unit -> unit
val add_external_library : string -> coq_module -> unit
(*s Read globalizations from a file (produced by coqc -dump-glob) *)
val read_glob : Digest.t option -> string -> unit
(*s Indexes *)
type 'a index = {
idx_name : string;
idx_entries : (char * (string * 'a) list) list;
idx_size : int }
val current_library : string ref
val display_letter : char -> string
val prepare_entry : string -> entry_type -> string
val all_entries : unit ->
(coq_module * entry_type) index *
(entry_type * coq_module index) list
val map : (string -> 'a -> 'b) -> 'a index -> 'b index
|