environement global

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@67 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 37 insertions, 0 deletions

diff --git a/library/global.ml b/library/global.ml
new file mode 100644
index 000000000..d669410b8
--- /dev/null
+++ b/library/global.ml
@@ -0,0 +1,37 @@
+
+(* $Id$ *)
+
+open 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 _ = 
+  declare_summary "Global environment"
+    { freeze_function = (fun () -> !global_env);
+      unfreeze_function = (fun fr -> global_env := fr);
+      init_function = (fun () -> global_env := empty_environment) }
+
+(* Then we export the functions of [Typing] on that environment. *)
+
+let evar_map () = evar_map !global_env
+let universes () = universes !global_env
+let metamap () = metamap !global_env
+let context () = context !global_env
+
+let push_var idc = global_env := push_var idc !global_env
+let push_rel nac = global_env := push_rel nac !global_env
+let add_constant sp ce = global_env := add_constant sp ce !global_env
+let add_parameter sp c = global_env := add_parameter sp c !global_env
+let add_mind sp mie = global_env := add_mind sp mie !global_env
+
+let lookup_var id = lookup_var id !global_env
+let lookup_rel n = lookup_rel n !global_env
+let lookup_constant sp = lookup_constant sp !global_env
+let lookup_mind sp = lookup_mind sp !global_env
+let lookup_mind_specif c = lookup_mind_specif c !global_env
+let lookup_meta n = lookup_meta n !global_env
+