summaryrefslogtreecommitdiff
path: root/contrib/xml/cic2acic.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2007-08-18 20:34:57 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2007-08-18 20:34:57 +0000
commit72b9a7df489ea47b3e5470741fd39f6100d31676 (patch)
tree60108a573d2a80d2dd4e3833649890e32427ff8d /contrib/xml/cic2acic.ml
parent55ce117e8083477593cf1ff2e51a3641c7973830 (diff)
Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg
Diffstat (limited to 'contrib/xml/cic2acic.ml')
-rw-r--r--contrib/xml/cic2acic.ml19
1 files changed, 13 insertions, 6 deletions
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index ff07c3c4..8a5967a2 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -22,8 +22,13 @@ let get_module_path_of_section_path path =
List.filter
(function modul -> Libnames.is_dirpath_prefix_of modul dirpath) modules
with
- [modul] -> modul
- | _ -> raise TwoModulesWhoseDirPathIsOneAPrefixOfTheOther
+ [] ->
+ Pp.warning ("Modules not supported: reference to "^
+ Libnames.string_of_path path^" will be wrong");
+ dirpath
+ | [modul] -> modul
+ | _ ->
+ raise TwoModulesWhoseDirPathIsOneAPrefixOfTheOther
;;
(*CSC: Problem: here we are using the wrong (???) hypothesis that there do *)
@@ -652,11 +657,13 @@ print_endline "PASSATO" ; flush stdout ;
A.ALambdas (new_passed_lambdas, t')
)
| T.LetIn (n,s,t,d) ->
- let n' =
+ let id =
match n with
- N.Anonymous -> N.Anonymous
- | _ ->
- N.Name (Nameops.next_name_away n (Termops.ids_of_context env))
+ N.Anonymous -> N.id_of_string "_X"
+ | N.Name id -> id
+ in
+ let n' =
+ N.Name (Nameops.next_ident_away id (Termops.ids_of_context env))
in
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
let sourcesort =