Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

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