blob: 6e302989fe43650fafcc5a5998da355b002da530 (
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
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
|
(*i $Id$ i*)
open Names
open Term
val add_ml_import : global_reference -> identifier -> unit
val is_ml_import : global_reference -> bool
val find_ml_import : global_reference -> identifier
val add_ml_extract : global_reference -> identifier -> unit
val find_ml_extract : global_reference -> identifier
val is_ml_extract : global_reference -> bool
(*
val list0n : int -> int list
val next_global_ident : Names.identifier -> Names.identifier
val ml_import_tab : (Term.sorts Term.oper, Names.identifier) Hashtabl.t
val mL_INDUCTIVES : Names.section_path list ref
val add_ml_inductive_import : Names.section_path -> unit
val sp_is_ml_import : Names.section_path -> bool
val sp_prod : Names.section_path
val sp_is_ml_import_or_prod : Names.section_path -> bool
val inMLImport : Term.sorts Term.oper * Names.identifier -> Libobject.obj
val outMLImport : Libobject.obj -> Term.sorts Term.oper * Names.identifier
val ml_extract_tab : (Term.sorts Term.oper, Names.identifier) Hashtabl.t
val sp_is_ml_extract : Names.section_path -> bool
val inMLExtract : Term.sorts Term.oper * Names.identifier -> Libobject.obj
val outMLExtract : Libobject.obj -> Term.sorts Term.oper * Names.identifier
val is_import_or_extract : Names.section_path -> bool
val freeze :
unit ->
(Term.sorts Term.oper, Names.identifier) Hashtabl.frozen_t *
Names.section_path list *
(Term.sorts Term.oper, Names.identifier) Hashtabl.frozen_t
val unfreeze :
(Term.sorts Term.oper, Names.identifier) Hashtabl.frozen_t *
Names.section_path list *
(Term.sorts Term.oper, Names.identifier) Hashtabl.frozen_t -> unit
val whd_fwify : 'a Term.oper Generic.term -> 'a Term.oper Generic.term
val fwify : Reduction.reduction_function
val fwsp_of_id : Names.identifier -> Names.section_path
val make_fw_parameter_body :
Term.type_judgement Names.signature * Term.type_judgement ->
Constrtypes.constant_body
val fw_infexecute_parameter :
Term.context ->
Names.identifier ->
Term.constr ->
Impuniv.universes * (Names.path_kind * Constrtypes.constant_body) list
val fw_machine_parameter :
Term.context -> Names.identifier * Term.constr -> unit
val fw_parameter : Names.identifier -> CoqAst.t -> unit
val ml_import : Names.identifier -> Names.identifier -> CoqAst.t -> unit
val id_of_varg : Vernacinterp.vernac_arg -> Names.identifier
val not_an_axiom : Names.identifier -> 'a
val not_have_type :
Term.environment ->
Constrtypes.constant_body -> Constrtypes.constant_body -> 'a
val fw_infexecute_constant :
Term.context ->
Names.identifier ->
Term.constr ->
Impuniv.universes * (Names.path_kind * Constrtypes.constant_body) list
val fw_link : Names.identifier -> CoqAst.t -> unit
val fw_machine_minductive :
Term.context ->
int ->
(Names.identifier * Names.name * Term.type_judgement * Term.constr *
Names.identifier array)
array -> bool -> unit
val fw_fconstruct :
'a Evd.evar_map -> Term.context -> CoqAst.t -> Term.type_judgement
val fw_build_mutual :
(Names.identifier * CoqAst.t) list ->
(Names.identifier * CoqAst.t * (Names.identifier * CoqAst.t) list) list ->
bool -> unit
val not_same_number_types : unit -> 'a
val not_same_number_constructors : Names.identifier * Names.identifier -> 'a
val ml_import_inductive :
(Names.identifier * Names.identifier list) list ->
(Names.identifier * CoqAst.t) list ->
(Names.identifier * CoqAst.t * (Names.identifier * CoqAst.t) list) list ->
bool -> unit
val extract_constant : Names.identifier -> Names.identifier -> unit
val extract_inductive :
Names.identifier -> Names.identifier * Names.identifier list -> unit
val fprint_recipe : Constrtypes.recipe ref option -> Pp.std_ppcmds
val fprint_name : Names.identifier -> Pp.std_ppcmds
*)
|
