blob: bbb77c85371ef62dd3852f4dfbbd8e0e320fd472 (
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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
open Util
open Names
open Term
open Sign
open Environ
open Safe_typing
open Summary
(* We introduce here the global environment of the system, and we declare it
as a synchronized table. *)
let global_env = ref empty_environment
let safe_env () = !global_env
let env () = env_of_safe_env !global_env
let _ =
declare_summary "Global environment"
{ freeze_function = (fun () -> !global_env);
unfreeze_function = (fun fr -> global_env := fr);
init_function = (fun () -> global_env := empty_environment);
survive_section = false }
(* Then we export the functions of [Typing] on that environment. *)
let universes () = universes (env())
let named_context () = named_context (env())
let push_named_assum a =
let (cst,env) = push_named_assum a !global_env in
global_env := env;
cst
let push_named_def d =
let (cst,env) = push_named_def d !global_env in
global_env := env;
cst
let pop_named_decls ids = global_env := pop_named_decls ids !global_env
let add_parameter sp c = global_env := add_parameter sp c !global_env
let add_constant sp ce = global_env := add_constant sp ce !global_env
let add_discharged_constant sp r =
global_env := add_discharged_constant sp r !global_env
let add_mind sp mie = global_env := add_mind sp mie !global_env
let add_constraints c = global_env := add_constraints c !global_env
let lookup_named id = lookup_named id (env())
let lookup_constant sp = lookup_constant sp (env())
let lookup_inductive ind = Inductive.lookup_mind_specif (env()) ind
let lookup_mind sp = lookup_mind sp (env())
let export s = export !global_env s
let import cenv = global_env := import cenv !global_env
(*s Function to get an environment from the constants part of the global
environment and a given context. *)
let env_of_context hyps =
reset_with_named_context hyps (env())
open Nametab
let type_of_reference env = function
| VarRef id -> let (_,_,t) = Environ.lookup_named id env in t
| ConstRef c -> Environ.constant_type env c
| IndRef ind -> Inductive.type_of_inductive env ind
| ConstructRef cstr -> Inductive.type_of_constructor env cstr
let type_of_global t = type_of_reference (env ()) t
|
