diff options
author | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
tree | dabcac548e299fee1da464c93b3dba98484f45b1 /library/global.ml | |
parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'library/global.ml')
-rw-r--r-- | library/global.ml | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/library/global.ml b/library/global.ml index ab5d8956..b2f9e127 100644 --- a/library/global.ml +++ b/library/global.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: global.ml 9310 2006-10-28 19:35:09Z herbelin $ *) +(* $Id: global.ml 10664 2008-03-14 11:27:37Z soubiran $ *) open Util open Names @@ -68,11 +68,14 @@ 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) () +let add_alias = add_thing (fun _ -> add_alias) () let add_constraints c = global_env := add_constraints c !global_env let set_engagement c = global_env := set_engagement c !global_env +let add_include me = global_env := add_include me !global_env + let start_module id = let l = label_of_id id in let mp,newenv = start_module l !global_env in @@ -151,3 +154,10 @@ let type_of_reference env = function Inductive.type_of_constructor cstr specif let type_of_global t = type_of_reference (env ()) t + + +(* spiwack: register/unregister functions for retroknowledge *) +let register field value by_clause = + let entry = kind_of_term value in + let senv = Safe_typing.register !global_env field entry by_clause in + global_env := senv |