diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-02-03 01:07:24 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-02-03 01:07:24 +0000 |
| commit | 0be378fdf6abd2ccc167463c2b0b020914ec7972 (patch) | |
| tree | ec8ae6a751f0b257380d5347574ecea17d654640 /contrib/extraction | |
| parent | e1f1f014a6ec724367c387582a7848182dad0ec7 (diff) | |
hack horrible pour renommage dans Modules Types et Functeurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3648 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction')
| -rw-r--r-- | contrib/extraction/common.ml | 43 |
1 files changed, 23 insertions, 20 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml index cc943280d..0b5b10e21 100644 --- a/contrib/extraction/common.ml +++ b/contrib/extraction/common.ml @@ -291,27 +291,30 @@ module StdParams = struct let mp = modpath (kn_of_r r) in let l,s = get_renamings r in let n = length_common_prefix cur_l l in - if n = 0 && !modular (* [r] is in another module *) - then - if (Refset.mem r !must_qualify) || (lang () = Haskell) - then str (string_of_ren l s) + if not (is_modfile (base_mp cur_mp)) && (is_modfile (base_mp mp)) then + str (string_of_ren (mp_to_list' mp) s) + else + if n = 0 && !modular (* [r] is in another module *) + then + if (Refset.mem r !must_qualify) || (lang () = Haskell) + then str (string_of_ren l s) + else + try + if clash_in_contents mp s (decreasing_contents cur_mp) + then str (string_of_ren l s) + else str s + with Not_found -> str (string_of_ren l s) else - try - if clash_in_contents mp s (decreasing_contents cur_mp) - then str (string_of_ren l s) - else str s - with Not_found -> str (string_of_ren l s) - else - let nl = List.length l in - if n = nl && nl < List.length cur_l then (* strict prefix *) - try - if clash_in_contents mp s (decreasing_contents cur_mp) - then error_unqualified_name (string_of_ren l s) (string_of_modlist cur_l) - else str s - with Not_found -> str (string_of_ren l s) - else (* [cur_mp] and [mp] are orthogonal *) - let l = remove_common cur_l l - in str (string_of_ren l s) + let nl = List.length l in + if n = nl && nl < List.length cur_l then (* strict prefix *) + try + if clash_in_contents mp s (decreasing_contents cur_mp) + then error_unqualified_name (string_of_ren l s) (string_of_modlist cur_l) + else str s + with Not_found -> str (string_of_ren l s) + else (* [cur_mp] and [mp] are orthogonal *) + let l = remove_common cur_l l + in str (string_of_ren l s) let pp_long_module cur_mp mp = let cur_mp = long_mp cur_mp in |