aboutsummaryrefslogtreecommitdiff
path: root/vernac/classes.mli
diff options
context:
space:
mode:
authorMaxime Dénès2018-06-01 13:49:34 +0200
committerMaxime Dénès2018-06-01 13:49:34 +0200
commit3a36761a27487e8917e1b59b59abacc2a7e65b95 (patch)
treef1cd9d412c40933ff3e87f720dbd8e7cba7f9bbf /vernac/classes.mli
parentac0bb15616550d00f5e6e7d6239e3b7ff2632975 (diff)
parent63b530234e0b19323a50c52434a7439518565c81 (diff)
Merge PR #7570: [api] Move `Constrexpr` to the `interp` module.
Diffstat (limited to 'vernac/classes.mli')
-rw-r--r--vernac/classes.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 631da8400a..eea2a211d8 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -32,7 +32,7 @@ val declare_instance_constant :
Impargs.manual_explicitation list -> (** implicits *)
?hook:(GlobRef.t -> unit) ->
Id.t -> (** name *)
- Univdecls.universe_decl ->
+ UState.universe_decl ->
bool -> (* polymorphic *)
Evd.evar_map -> (* Universes *)
Constr.t -> (** body *)