diff options
| author | Pierre-Marie Pédrot | 2019-11-16 15:09:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-11-16 15:09:17 +0100 |
| commit | 64265294b519d7cd9f982edf24991c7f210933a9 (patch) | |
| tree | aa058ca9c2ecc32162ec0f0d4cf721f19ae95cf8 /vernac/classes.mli | |
| parent | 6045fcf7398c4098566f7da5c4cba808c7416788 (diff) | |
| parent | 95c47ad501bdfb996858c64eee1b4545ef3f5acb (diff) | |
Merge PR #10996: Refine Instance returns
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: ppedrot
Diffstat (limited to 'vernac/classes.mli')
| -rw-r--r-- | vernac/classes.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/vernac/classes.mli b/vernac/classes.mli index 1247fdc8c1..594df52c70 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -35,6 +35,7 @@ val new_instance_interactive -> ?tac:unit Proofview.tactic -> ?hook:(GlobRef.t -> unit) -> Hints.hint_info_expr + -> (bool * constr_expr) option -> Id.t * Lemmas.t val new_instance @@ -84,3 +85,5 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u (** For generation on names based on classes only *) val id_of_class : typeclass -> Id.t + +val refine_att : bool Attributes.attribute |