diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:28 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:28 -0500 |
commit | 1ef7f1c0c6897535a86daa77799714e25638f5e9 (patch) | |
tree | 5bcca733632ecc84d2c6b1ee48cb2e557a7adba5 /vernac/classes.mli | |
parent | 3a2fac7bcee36fd9dcb4f39a615c8ac0349abcc9 (diff) | |
parent | 9ebf44d84754adc5b64fcf612c6816c02c80462d (diff) |
Updated version 8.9.0 from 'upstream/8.9.0'
with Debian dir 81a4f85bc45e59aa1eadb4797f0eb0b8039efb63
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 *) |