diff options
| author | Enrico Tassi | 2021-03-05 15:23:04 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2021-03-05 15:23:04 +0100 |
| commit | 220e54a9cfa4d9f5da550542a8b6ca5ab90c1698 (patch) | |
| tree | d0d709ba0ccf619ac8bc19870dc7b9718bfd177d /pretyping/coercionops.mli | |
| parent | a5bea627d1fe742229497b466ca24b470c20d269 (diff) | |
[coercipn] expose coercion_info
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 *) |