From 248728628f5da946f96c22ba0a0e7e9b33019382 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 19 Feb 2013 20:27:51 +0000 Subject: Dir_path --> DirPath Ok, this is merely a matter of taste, but up to now the usage in Coq is rather to use capital letters instead of _ in the names of inner modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/safe_typing.mli | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'kernel/safe_typing.mli') diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 7cddde954..1bb43a53e 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -43,12 +43,12 @@ type global_declaration = | GlobalRecipe of Cooking.recipe val add_constant : - Dir_path.t -> Label.t -> global_declaration -> safe_environment -> + DirPath.t -> Label.t -> global_declaration -> safe_environment -> constant * safe_environment (** Adding an inductive type *) val add_mind : - Dir_path.t -> Label.t -> mutual_inductive_entry -> safe_environment -> + DirPath.t -> Label.t -> mutual_inductive_entry -> safe_environment -> mutual_inductive * safe_environment (** Adding a module *) @@ -103,10 +103,10 @@ type compiled_library type native_library = Nativecode.global list -val start_library : Dir_path.t -> safe_environment +val start_library : DirPath.t -> safe_environment -> module_path * safe_environment -val export : safe_environment -> Dir_path.t +val export : safe_environment -> DirPath.t -> module_path * compiled_library * native_library val import : compiled_library -> Digest.t -> safe_environment -- cgit v1.2.3