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 | |
| parent | a5bea627d1fe742229497b466ca24b470c20d269 (diff) | |
[coercipn] expose coercion_info
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 *) |