From 220e54a9cfa4d9f5da550542a8b6ca5ab90c1698 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 5 Mar 2021 15:23:04 +0100
Subject: [coercipn] expose coercion_info

---
 pretyping/coercionops.ml  | 2 --
 pretyping/coercionops.mli | 2 ++
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping')

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 *)
-- 
cgit v1.2.3