diff options
Diffstat (limited to 'toplevel/classes.mli')
| -rw-r--r-- | toplevel/classes.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/toplevel/classes.mli b/toplevel/classes.mli index de62ff369..4dd62ba9f 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -36,13 +36,16 @@ val declare_instance_constant : Impargs.manual_explicitation list -> (** implicits *) ?hook:(Globnames.global_reference -> unit) -> Id.t -> (** name *) - Entries.proof_output -> (** body *) + bool -> (* polymorphic *) + Univ.universe_context -> (* Universes *) + Constr.t -> (** body *) Term.types -> (** type *) Names.Id.t val new_instance : ?abstract:bool -> (** Not abstract by default. *) ?global:bool -> (** Not global by default. *) + Decl_kinds.polymorphic -> local_binder list -> typeclass_constraint -> constr_expr option -> |