aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/record.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/record.mli')
-rw-r--r--vernac/record.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/record.mli b/vernac/record.mli
index 308c9e9b9..b2c039f0b 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -20,7 +20,7 @@ val declare_projections :
?kind:Decl_kinds.definition_object_kind ->
Id.t ->
bool list ->
- Universes.universe_binders ->
+ UnivNames.universe_binders ->
Impargs.manual_implicits list ->
Context.Rel.t ->
(Name.t * bool) list * Constant.t option list