From 3386a50c15ddc367cd247f288ff84f288a0c42af Mon Sep 17 00:00:00 2001
From: filliatr
Date: Sat, 18 Sep 1999 16:13:36 +0000
Subject: module Library

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@74 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/typing.ml  | 2 ++
 kernel/typing.mli | 3 +++
 2 files changed, 5 insertions(+)

(limited to 'kernel')

diff --git a/kernel/typing.ml b/kernel/typing.ml
index 7cd127cf60..1fcf340f3b 100644
--- a/kernel/typing.ml
+++ b/kernel/typing.ml
@@ -421,6 +421,8 @@ let add_mind sp mie env =
   in
   add_mind sp mib (set_universes (universes env_arities') env)
 
+let export = export
+let import = import
 
 (*s Machines with information. *)
 
diff --git a/kernel/typing.mli b/kernel/typing.mli
index d9d410c542..0167c8cd9c 100644
--- a/kernel/typing.mli
+++ b/kernel/typing.mli
@@ -41,6 +41,9 @@ val lookup_mind : section_path -> 'a environment -> mutual_inductive_body
 val lookup_mind_specif : constr -> 'a environment -> mind_specif
 val lookup_meta : int -> 'a environment -> constr
 
+val export : 'a environment -> string -> compiled_env
+val import : compiled_env -> 'a environment -> 'a environment
+
 (*s Typing without information. *)
 
 type judgment
-- 
cgit v1.2.3