diff options
Diffstat (limited to 'toplevel/classes.mli')
| -rw-r--r-- | toplevel/classes.mli | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 24c51b31..d2cb788e 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Context open Environ open Constrexpr open Typeclasses @@ -15,24 +14,25 @@ open Libnames (** Errors *) -val mismatched_params : env -> constr_expr list -> rel_context -> 'a +val mismatched_params : env -> constr_expr list -> Context.Rel.t -> 'a -val mismatched_props : env -> constr_expr list -> rel_context -> 'a +val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a (** Instance declaration *) -val existing_instance : bool -> reference -> int option -> unit -(** globality, reference, priority *) +val existing_instance : bool -> reference -> Vernacexpr.hint_info_expr option -> unit +(** globality, reference, optional priority and pattern information *) val declare_instance_constant : typeclass -> - int option -> (** priority *) + Vernacexpr.hint_info_expr -> (** priority *) bool -> (** globality *) Impargs.manual_explicitation list -> (** implicits *) ?hook:(Globnames.global_reference -> unit) -> Id.t -> (** name *) + Id.t Loc.located list option -> bool -> (* polymorphic *) - Univ.universe_context_set -> (* Universes *) + Evd.evar_map -> (* Universes *) Constr.t -> (** body *) Term.types -> (** type *) Names.Id.t @@ -40,6 +40,7 @@ val declare_instance_constant : val new_instance : ?abstract:bool -> (** Not abstract by default. *) ?global:bool -> (** Not global by default. *) + ?refine:bool -> (** Allow refinement *) Decl_kinds.polymorphic -> local_binder list -> typeclass_constraint -> @@ -47,7 +48,7 @@ val new_instance : ?generalize:bool -> ?tac:unit Proofview.tactic -> ?hook:(Globnames.global_reference -> unit) -> - int option -> + Vernacexpr.hint_info_expr -> Id.t (** Setting opacity *) |