diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-06-12 22:46:21 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-06-12 22:46:21 +0000 |
| commit | 9bb177741ecc1b706876b8c9a329c3e1530944b4 (patch) | |
| tree | 0eaa065e07e71d3e9595f61e9586f9ea52017dae | |
| parent | bf5866e8be3cf42455a6763ce967e690e8115f46 (diff) | |
enieme correction du nommage modulaire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4143 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/extraction/common.ml | 28 | ||||
| -rw-r--r-- | contrib/extraction/modutil.ml | 2 |
2 files changed, 20 insertions, 10 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml index 09a58648e..f7767f46d 100644 --- a/contrib/extraction/common.ml +++ b/contrib/extraction/common.ml @@ -252,11 +252,16 @@ module StdParams = struct with Not_found -> (* [mp] is othogonal with every element of [mp]. *) let base, l = labels_of_mp mp in let short = string_of_ren (print_labels l) s in - if not (at_toplevel mp) || - (!modular && - (l <> [] || (Refset.mem r !to_qualify) || (clash base l s mpl))) - then (print_base_mp base)^"."^short - else short + if !modular then + if (at_toplevel mp) && + not (Refset.mem r !to_qualify) && + not (clash base [] s mpl) + then short + else (print_base_mp base)^"."^short + else + if (at_toplevel base) + then short + else (print_base_mp base)^"."^short in add_module_contents mp s; (* update the visible environment *) str final @@ -273,11 +278,16 @@ module StdParams = struct i*) str (string_of_modlist (print_labels l)) with Not_found -> (* [mp] is othogonal with every element of [mp]. *) - let base_mp, l = labels_of_mp mp in + let base, l = labels_of_mp mp in let short = string_of_modlist (print_labels l) in - if not (at_toplevel mp) || !modular - then str ((print_base_mp base_mp)^(if short = "" then "" else "."^short)) - else str short + if !modular then + if (at_toplevel mp) + then str short + else str ((print_base_mp base)^(if short = "" then "" else "."^short)) + else + if (at_toplevel base) + then str short + else str ((print_base_mp base)^(if short = "" then "" else "."^short)) let pp_short_module id = str (rename_module id) end diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml index 343861ee4..245318107 100644 --- a/contrib/extraction/modutil.ml +++ b/contrib/extraction/modutil.ml @@ -107,7 +107,7 @@ let rec modfile_of_mp mp = match mp with | _ -> raise Not_found let rec fst_level_module_of_mp mp = match mp with - | MPdot (mp, l) when is_toplevel mp -> mp,l + | MPdot (mp, l) when at_toplevel mp -> mp,l | MPdot (mp, l) -> fst_level_module_of_mp mp | _ -> raise Not_found |