X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcoercDb.mli;h=d8a8b0574de506f222da61acfb073f9074723896;hb=d5c1f34cd226898525168e470d3e2ec273699826;hp=92d4b7f2484e231e1547a62899fe094ece785c79;hpb=6fb856f244035ba071d60a158fa800104f50072a;p=helm.git diff --git a/helm/software/components/library/coercDb.mli b/helm/software/components/library/coercDb.mli index 92d4b7f24..d8a8b0574 100644 --- a/helm/software/components/library/coercDb.mli +++ b/helm/software/components/library/coercDb.mli @@ -36,6 +36,8 @@ type coerc_carr = | Uri of UriManager.uri (* const, mutind, mutconstr *) | Sort of Cic.sort (* Prop, Set, Type *) | Term of Cic.term (* nothing supported *) + | Fun of int +;; exception EqCarrNotImplemented of string Lazy.t exception EqCarrOnNonMetaClosed