diff options
| -rw-r--r-- | interp/constrintern.ml | 12 | ||||
| -rw-r--r-- | lib/util.ml | 14 | ||||
| -rw-r--r-- | lib/util.mli | 1 | ||||
| -rw-r--r-- | library/libnames.ml | 6 | ||||
| -rw-r--r-- | library/libnames.mli | 1 |
5 files changed, 26 insertions, 8 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 98919082d..9e6cbaf44 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -140,12 +140,12 @@ let coqdoc_unfreeze (lt,tn,lp) = let add_glob loc ref = let sp = Nametab.sp_of_global ref in - let modqid,id = repr_path sp in - let file_prefix_length = List.length (repr_dirpath (Lib.library_dp())) in - let file,fields = chop_dirpath file_prefix_length modqid in - let filepath = string_of_dirpath file in - let modpath = string_of_qualid (make_qualid fields id) in - dump_string (Printf.sprintf "R%d %s.%s\n" (fst (unloc loc)) filepath modpath) + let lib_dp = Lib.library_dp() in + let mod_dp,id = repr_path sp in + let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in + let filepath = string_of_dirpath lib_dp in + let fullname = string_of_qualid (make_qualid mod_dp_trunc id) in + dump_string (Printf.sprintf "R%d %s.%s\n" (fst (unloc loc)) filepath fullname) let loc_of_notation f loc args ntn = if args=[] or ntn.[0] <> '_' then fst (unloc loc) diff --git a/lib/util.ml b/lib/util.ml index 04086e20f..a9d9655ed 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -363,7 +363,19 @@ let list_prefix_of prefl l = | ([], _) -> true | (_, _) -> false in - prefrec (prefl,l) + prefrec (prefl,l) + +let list_drop_prefix p l = +(* if l=p++t then return t else l *) + let rec list_drop_prefix_rec = function + | ([], tl) -> Some tl + | (_, []) -> None + | (h1::tp, h2::tl) -> + if h1 = h2 then list_drop_prefix_rec (tp,tl) else None + in + match list_drop_prefix_rec (p,l) with + | Some r -> r + | None -> l let list_map_append f l = List.flatten (List.map f l) diff --git a/lib/util.mli b/lib/util.mli index ababb2ff9..e93094f89 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -123,6 +123,7 @@ val list_last : 'a list -> 'a val list_lastn : int -> 'a list -> 'a list val list_skipn : int -> 'a list -> 'a list val list_prefix_of : 'a list -> 'a list -> bool +val list_drop_prefix : 'a list -> 'a list -> 'a list (* [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *) val list_map_append : ('a -> 'b list) -> 'a list -> 'b list (* raises [Invalid_argument] if the two lists don't have the same length *) diff --git a/library/libnames.ml b/library/libnames.ml index d4cc60719..424cf1f73 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -80,7 +80,11 @@ let is_dirpath_prefix_of d1 d2 = let chop_dirpath n d = let d1,d2 = list_chop n (List.rev (repr_dirpath d)) in - make_dirpath (List.rev d1), make_dirpath (List.rev d2) + make_dirpath (List.rev d1), make_dirpath (List.rev d2) + +let drop_dirpath_prefix d1 d2 = + let d = Util.list_drop_prefix (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) in + make_dirpath (List.rev d) (* To know how qualified a name should be to be understood in the current env*) let add_dirpath_prefix id d = make_dirpath (repr_dirpath d @ [id]) diff --git a/library/libnames.mli b/library/libnames.mli index 22cdd3a09..69710f431 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -54,6 +54,7 @@ val extend_dirpath : dir_path -> module_ident -> dir_path val add_dirpath_prefix : module_ident -> dir_path -> dir_path val chop_dirpath : int -> dir_path -> dir_path * dir_path +val drop_dirpath_prefix : dir_path -> dir_path -> dir_path val extract_dirpath_prefix : int -> dir_path -> dir_path val is_dirpath_prefix_of : dir_path -> dir_path -> bool |