X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.mli;h=a195a2fd8d55cfcaf7bd88e7946655d3f0fa6fab;hb=117dfe4f3b6d8ebf53172eaf66b628a27e4e43e1;hp=fd101414df75853f61fe6eabb926ead6ab559036;hpb=9d33fd0863f207cee7f882ae28c83e1944d2a0f1;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli
index fd101414d..a195a2fd8 100644
--- a/helm/software/components/ng_refiner/nCicMetaSubst.mli
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli
@@ -67,5 +67,7 @@ val saturate:
     NCic.context -> NCic.term -> int ->
        NCic.term * NCic.metasenv * NCic.term list
 
+val pack_lc : int * NCic.lc_kind -> int * NCic.lc_kind
+
 val is_out_scope_tag : NCic.meta_attrs -> bool
 val int_of_out_scope_tag : NCic.meta_attrs -> int