diff options
| author | Pierre-Marie Pédrot | 2021-03-06 10:56:25 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-06 10:56:25 +0100 |
| commit | c738d6540ddadaa29ea6b3181f6ee462792fe9ce (patch) | |
| tree | b3fc0859ccf3d65f7993ec78936229601db82935 /pretyping | |
| parent | 8a61edf00c8f219fff852b70fb9c74e5d3e2aca1 (diff) | |
| parent | 220e54a9cfa4d9f5da550542a8b6ca5ab90c1698 (diff) | |
Merge PR #13902: [coercion] expose coercion_info
Reviewed-by: ppedrot
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/coercionops.ml | 2 | ||||
| -rw-r--r-- | pretyping/coercionops.mli | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml index 8ddc576d83..ac89dfd747 100644 --- a/pretyping/coercionops.ml +++ b/pretyping/coercionops.ml @@ -156,8 +156,6 @@ let cl_fun_index = fst(class_info CL_FUN) let cl_sort_index = fst(class_info CL_SORT) -(* coercion_info : coe_typ -> coe_info_typ *) - let coercion_info coe = CoeTypMap.find coe !coercion_tab let coercion_exists coe = CoeTypMap.mem coe !coercion_tab 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 *) |