diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /toplevel/classes.mli | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
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 *) |