diff options
| author | Emilio Jesus Gallego Arias | 2019-02-24 20:38:21 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-17 12:30:13 +0200 |
| commit | 873281c256fc33941d93044acc3db8eda0a148ee (patch) | |
| tree | 2104c16c197b2cc9a8c9cc903818691b6eb1a3a7 /vernac/class.mli | |
| parent | 7dc04f0244aeb277b62070f87590cbc2cafd8396 (diff) | |
[proof] Move declaration hooks to DeclareDef.
This way both `Lemmas` and `DeclareObl` can depend on it, removing one
more difficulty on the unification of terminators.
Diffstat (limited to 'vernac/class.mli')
| -rw-r--r-- | vernac/class.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/class.mli b/vernac/class.mli index 80d6d4383c..85266739ad 100644 --- a/vernac/class.mli +++ b/vernac/class.mli @@ -42,8 +42,8 @@ val try_add_new_coercion_with_source : GlobRef.t -> local:bool -> val try_add_new_identity_coercion : Id.t -> local:bool -> Decl_kinds.polymorphic -> source:cl_typ -> target:cl_typ -> unit -val add_coercion_hook : Decl_kinds.polymorphic -> Lemmas.declaration_hook +val add_coercion_hook : Decl_kinds.polymorphic -> DeclareDef.Hook.t -val add_subclass_hook : Decl_kinds.polymorphic -> Lemmas.declaration_hook +val add_subclass_hook : Decl_kinds.polymorphic -> DeclareDef.Hook.t val class_of_global : GlobRef.t -> cl_typ |