diff options
Diffstat (limited to 'pretyping/coercionops.mli')
| -rw-r--r-- | pretyping/coercionops.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/coercionops.mli b/pretyping/coercionops.mli index 31600dd17f..073500b155 100644 --- a/pretyping/coercionops.mli +++ b/pretyping/coercionops.mli @@ -92,6 +92,8 @@ val declare_coercion : env -> evar_map -> coercion -> unit (** {6 Access to coercions infos } *) val coercion_exists : coe_typ -> bool +val coercion_info : coe_typ -> coe_info_typ + (** {6 Lookup functions for coercion paths } *) (** @raise Not_found in the following functions when no path exists *) |