diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /vernac/classes.mli | |
parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) |
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'vernac/classes.mli')
-rw-r--r-- | vernac/classes.mli | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/vernac/classes.mli b/vernac/classes.mli index 0342c840..9c37364c 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -16,23 +16,23 @@ open Libnames (** Errors *) -val mismatched_params : env -> constr_expr list -> Context.Rel.t -> 'a +val mismatched_params : env -> constr_expr list -> Constr.rel_context -> 'a -val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a +val mismatched_props : env -> constr_expr list -> Constr.rel_context -> 'a (** Instance declaration *) -val existing_instance : bool -> reference -> Vernacexpr.hint_info_expr option -> unit +val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit (** globality, reference, optional priority and pattern information *) val declare_instance_constant : typeclass -> - Vernacexpr.hint_info_expr -> (** priority *) + Hints.hint_info_expr -> (** priority *) bool -> (** globality *) Impargs.manual_explicitation list -> (** implicits *) - ?hook:(Globnames.global_reference -> unit) -> + ?hook:(GlobRef.t -> unit) -> Id.t -> (** name *) - Univdecls.universe_decl -> + UState.universe_decl -> bool -> (* polymorphic *) Evd.evar_map -> (* Universes *) Constr.t -> (** body *) @@ -50,8 +50,8 @@ val new_instance : (bool * constr_expr) option -> ?generalize:bool -> ?tac:unit Proofview.tactic -> - ?hook:(Globnames.global_reference -> unit) -> - Vernacexpr.hint_info_expr -> + ?hook:(GlobRef.t -> unit) -> + Hints.hint_info_expr -> Id.t (** Setting opacity *) |