diff options
| author | Emilio Jesus Gallego Arias | 2018-09-18 20:40:51 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-09-29 19:11:31 +0200 |
| commit | 1c82abbdec8df7cccc886db74ca1c9f596302ce1 (patch) | |
| tree | eba09482d20b5613675eca144b34f404bf11f667 /vernac/classes.mli | |
| parent | 081326a7b2c64e8620777aeae7e2275144b65b4b (diff) | |
[classes] Split large `new_instance` function up.
`Classes.new_instance` is one of the largest functions of the
codebase; we split it up and reduce indentation.
This will help further cleanups. This PR should introduce no code
changes other than splitting the function up.
Diffstat (limited to 'vernac/classes.mli')
| -rw-r--r-- | vernac/classes.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/classes.mli b/vernac/classes.mli index 9c37364cb0..bb70334342 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -37,7 +37,7 @@ val declare_instance_constant : Evd.evar_map -> (* Universes *) Constr.t -> (** body *) Constr.types -> (** type *) - Names.Id.t + unit val new_instance : ?abstract:bool -> (** Not abstract by default. *) |