diff options
| author | Hugo Herbelin | 2018-10-19 23:34:24 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-19 23:34:24 +0200 |
| commit | 02f7b4ac1968ca4522d144e34b52dead3871a8b7 (patch) | |
| tree | 1e649e34972959b77eeebd4c5c6237fd12af1f61 /library | |
| parent | 3799939088b5aa616974a0d37de7e2616024f222 (diff) | |
| parent | 4ac1e342fe420e0b3f3adc9e619d2e98eba2111d (diff) | |
Merge PR #8758: [api] Qualify access to `Nametab`
Diffstat (limited to 'library')
| -rw-r--r-- | library/coqlib.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml index 677515981a..a044a9a395 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -14,7 +14,6 @@ open Pp open Names open Libnames open Globnames -open Nametab let make_dir l = DirPath.make (List.rev_map Id.of_string l) @@ -79,7 +78,7 @@ let register_ref s c = (* Generic functions to find Coq objects *) let has_suffix_in_dirs dirs ref = - let dir = dirpath (path_of_global ref) in + let dir = dirpath (Nametab.path_of_global ref) in List.exists (fun d -> is_dirpath_prefix_of d dir) dirs let gen_reference_in_modules locstr dirs s = |