diff options
Diffstat (limited to 'pretyping/coercionops.ml')
| -rw-r--r-- | pretyping/coercionops.ml | 2 |
1 files changed, 0 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 |