blob: 56a3cd11654485d9b9221a7fae6faba3dac17e45 (
plain)
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: index.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
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
| Mod of coq_module * string
val find : coq_module -> loc -> index_entry
val find_string : coq_module -> string -> index_entry
val add_module : coq_module -> unit
type module_kind = Local | Coqlib | Unknown
val find_module : coq_module -> module_kind
(*s Scan identifiers introductions from a file *)
val scan_file : string -> coq_module -> unit
(*s Read globalizations from a file (produced by coqc -dump-glob) *)
val read_glob : string -> coq_module
(*s Indexes *)
type 'a index = {
idx_name : string;
idx_entries : (char * (string * 'a) list) list;
idx_size : int }
val current_library : string ref
val all_entries : unit ->
(coq_module * entry_type) index *
(entry_type * coq_module index) list
val map : (string -> 'a -> 'b) -> 'a index -> 'b index
|
