summaryrefslogtreecommitdiff
path: root/vernac/comDefinition.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/comDefinition.mli')
-rw-r--r--vernac/comDefinition.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 6f81c457..7f1c902c 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -29,4 +29,4 @@ val do_definition : program_mode:bool ->
val interp_definition :
universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map *
- Univdecls.universe_decl * Impargs.manual_implicits
+ UState.universe_decl * Impargs.manual_implicits