aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/univdecls.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/univdecls.mli')
-rw-r--r--pretyping/univdecls.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/univdecls.mli b/pretyping/univdecls.mli
index 0c3b749cb..706d3a157 100644
--- a/pretyping/univdecls.mli
+++ b/pretyping/univdecls.mli
@@ -8,7 +8,7 @@
(** Local universe and constraint declarations. *)
type universe_decl =
- (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+ (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
val default_univ_decl : universe_decl