blob: e833d0bb806f484f62164ddc2f45be742f6acd09 (
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
|
(* $Id$ *)
(*i*)
open Names
open Term
open Constant
open Inductive
(*i*)
(* This module provides the official functions to declare new variables,
parameters, constants and inductive types. Using the following functions
will add the entries in the global environment (module [Global]), will
register the declarations in the library (module [Lib]) --- so that the
reset works properly --- and will fill some global tables such as
[Nametab] and [Impargs]. *)
type strength =
| DischargeAt of section_path
| NeverDischarge
val declare_variable : identifier -> constr -> unit
val declare_parameter : identifier -> constr -> unit
val declare_constant : identifier -> constant_entry -> unit
val declare_mind : mutual_inductive_entry -> unit
val declare_eliminations : section_path -> unit
(*s It also provides a function [global_reference] to construct a global
constr (a constant, an inductive or a constructor) from an identifier.
To do so, it first looks for the section path using [Nametab.sp_of_id] and
then constructs the corresponding term, associated to the current
environment of variables. *)
val global_reference : path_kind -> identifier -> constr
val is_global : identifier -> bool
val mind_path : constr -> section_path
|
