diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-19 20:27:51 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-19 20:27:51 +0000 |
| commit | 248728628f5da946f96c22ba0a0e7e9b33019382 (patch) | |
| tree | 905dbbafa65dd7bf02823318326be2ca389f833f /kernel/safe_typing.mli | |
| parent | 3889c9a9e7d017ef2eea647d8c17d153a0b90083 (diff) | |
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
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 8 |
1 files changed, 4 insertions, 4 deletions
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 |