diff options
Diffstat (limited to 'library/libnames.ml')
| -rw-r--r-- | library/libnames.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/libnames.ml b/library/libnames.ml index 37ae97ace..f3e8d17f3 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -153,8 +153,8 @@ type global_dir_reference = (* this won't last long I hope! *) type reference = - | Qualid of qualid located - | Ident of identifier located + | Qualid of qualid Loc.located + | Ident of identifier Loc.located let qualid_of_reference = function | Qualid (loc,qid) -> loc, qid |