aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/global.ml
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-17 15:58:14 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-17 15:58:14 +0000
commit61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch)
tree961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /library/global.ml
parent6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff)
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/global.ml')
-rw-r--r--library/global.ml20
1 files changed, 10 insertions, 10 deletions
diff --git a/library/global.ml b/library/global.ml
index ec41c0706..e228de23a 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -27,7 +27,7 @@ let env () = env_of_safe_env !global_env
let env_is_empty () = is_empty !global_env
-let _ =
+let _ =
declare_summary "Global environment"
{ freeze_function = (fun () -> !global_env);
unfreeze_function = (fun fr -> global_env := fr);
@@ -57,12 +57,12 @@ let push_named_def d =
anomaly "Kernel names do not match."
*)
-let add_thing add dir id thing =
+let add_thing add dir id thing =
let kn, newenv = add dir (label_of_id id) thing !global_env in
global_env := newenv;
kn
-let add_constant = add_thing add_constant
+let add_constant = add_thing add_constant
let add_mind = add_thing add_mind
let add_modtype = add_thing (fun _ -> add_modtype) ()
let add_module = add_thing (fun _ -> add_module) ()
@@ -120,16 +120,16 @@ let lookup_modtype kn = lookup_modtype kn (env())
-let start_library dir =
+let start_library dir =
let mp,newenv = start_library dir !global_env in
- global_env := newenv;
+ global_env := newenv;
mp
let export s = snd (export !global_env s)
-let import cenv digest =
- let mp,newenv = import cenv digest !global_env in
- global_env := newenv;
+let import cenv digest =
+ let mp,newenv = import cenv digest !global_env in
+ global_env := newenv;
mp
@@ -137,13 +137,13 @@ let import cenv digest =
(*s Function to get an environment from the constants part of the global
environment and a given context. *)
-let env_of_context hyps =
+let env_of_context hyps =
reset_with_named_context hyps (env())
open Libnames
let type_of_reference env = function
- | VarRef id -> Environ.named_type id env
+ | VarRef id -> Environ.named_type id env
| ConstRef c -> Typeops.type_of_constant env c
| IndRef ind ->
let specif = Inductive.lookup_mind_specif env ind in