COERCIONS: tentative addition of an equivalence relation over coercion source

[helm.git] / components / library / coercDb.mli

diff --git a/components/library/coercDb.mli b/components/library/coercDb.mli
index 5f455c2af97dd6146bddeebd64c0f281ce0b6334..e6d7e46b30042778b6b3889970c56dac329741bd 100644 (file)
--- a/components/library/coercDb.mli
+++ b/components/library/coercDb.mli
@@ -41,7 +41,7 @@ type coerc_carr =
   
 exception EqCarrNotImplemented of string Lazy.t
 exception EqCarrOnNonMetaClosed
-val eq_carr: coerc_carr -> coerc_carr -> bool
+val eq_carr: ?exact:bool -> coerc_carr -> coerc_carr -> bool
 val coerc_carr_of_term: Cic.term -> coerc_carr
 val name_of_carr: coerc_carr -> string
 val uri_of_carr: coerc_carr -> UriManager.uri option