blob: 21486c250e22dd2dc96d210a153ebb04f519d2ae (
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
|
(* $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 as [Nametab] and
[Impargs]. *)
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
|
