aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/libnames.mli
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-06-22 15:14:30 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-06-22 15:14:30 +0000
commit6b45f2d36929162cf92272bb60c2c245d9a0ead3 (patch)
tree93aa975697b7de73563c84773d99b4c65b92173b /library/libnames.mli
parentfea214f82954197d23fda9a0e4e7d93e0cbf9b4c (diff)
Added an indirection with respect to Loc in Compat. As many [open Compat]
were closed (i.e. the only remaining ones are those of printing/parsing). Meanwhile, a simplified interface is provided in loc.mli. This also permits to put Pp in Clib, because it does not depend on CAMLP4/5 anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/libnames.mli')
-rw-r--r--library/libnames.mli3
1 files changed, 2 insertions, 1 deletions
diff --git a/library/libnames.mli b/library/libnames.mli
index 24bdd2048..227d1f3df 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -7,6 +7,7 @@
(************************************************************************)
open Pp
+open Loc
open Names
(** {6 Dirpaths } *)
@@ -109,7 +110,7 @@ type reference =
val qualid_of_reference : reference -> qualid located
val string_of_reference : reference -> string
val pr_reference : reference -> std_ppcmds
-val loc_of_reference : reference -> loc
+val loc_of_reference : reference -> Loc.t
(** Deprecated synonyms *)