aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/safe_typing.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/safe_typing.mli')
-rw-r--r--kernel/safe_typing.mli6
1 files changed, 4 insertions, 2 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index ce62eeafc..3e1051088 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -12,8 +12,9 @@ open Declarations
open Entries
open Mod_subst
-(** {6 Sect } *)
-(** Safe environments. Since we are now able to type terms, we can
+(** {6 Safe environments } *)
+
+(** Since we are now able to type terms, we can
define an abstract type of safe environments, where objects are
typed before being added.
@@ -69,6 +70,7 @@ val set_engagement : engagement -> safe_environment -> safe_environment
(** {6 Interactive module functions } *)
+
val start_module :
label -> safe_environment -> module_path * safe_environment