diff options
Diffstat (limited to 'toplevel/class.mli')
| -rw-r--r-- | toplevel/class.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/class.mli b/toplevel/class.mli index 671219c3c..8311be4a5 100644 --- a/toplevel/class.mli +++ b/toplevel/class.mli @@ -46,9 +46,9 @@ val try_add_new_coercion_with_source : global_reference -> strength -> val try_add_new_identity_coercion : identifier -> strength -> source:cl_typ -> target:cl_typ -> unit -val add_coercion_hook : Proof_type.declaration_hook +val add_coercion_hook : Tacexpr.declaration_hook -val add_subclass_hook : Proof_type.declaration_hook +val add_subclass_hook : Tacexpr.declaration_hook (* [try_add_new_class ref] declares [ref] as a new class; usually, this is done implicitely by [try_add_new_coercion]'s functions *) |