diff options
| author | herbelin | 2001-10-17 12:49:19 +0000 |
|---|---|---|
| committer | herbelin | 2001-10-17 12:49:19 +0000 |
| commit | a6d858b84132bcb27bcc771f06a854cc94eef716 (patch) | |
| tree | df016a77a6d8d2f2a43fa9c2c01adc09b3be7c1b /contrib/extraction | |
| parent | 000ece141dc22e35365ea81558e8b6b1e65bd54c (diff) | |
Abstraction de l'immplementation de dirpath et implementation dans l'autre sens pour plus de partage entre chemins
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2126 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction')
| -rw-r--r-- | contrib/extraction/extract_env.ml | 2 | ||||
| -rw-r--r-- | contrib/extraction/ocaml.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index 68ff965b25..d726d4fa33 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -229,7 +229,7 @@ let _ = those having an ML extraction. *) let extract_module m = - let m = Nametab.locate_loaded_library (Nametab.make_qualid [] m) in + let m = Nametab.locate_loaded_library (Nametab.make_short_qualid m) in let seg = Library.module_segment (Some m) in let get_reference = function | sp, Leaf o -> diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index 1bc47b1e0d..81d77741b0 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -82,7 +82,7 @@ let rename_upper_global id = rename_global (uppercase_id id) (*s Modules considerations *) -let module_of_r r = list_last (dirpath (sp_of_r r)) +let module_of_r r = snd (split_dirpath (dirpath (sp_of_r r))) let string_of_r r = string_of_id (basename (sp_of_r r)) |