aboutsummaryrefslogtreecommitdiff
path: root/kernel/univ.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/univ.mli')
-rw-r--r--kernel/univ.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 7286fc84cb..eeaa1ad62d 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -15,8 +15,8 @@ sig
module UGlobal : sig
type t
- val make : Names.DirPath.t -> int -> t
- val repr : t -> Names.DirPath.t * int
+ val make : Names.DirPath.t -> string -> int -> t
+ val repr : t -> Names.DirPath.t * string * int
val equal : t -> t -> bool
val hash : t -> int
val compare : t -> t -> int