X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.mli;h=fd101414df75853f61fe6eabb926ead6ab559036;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=1c96577a74121d90639bbc6905dd7345bd5d647a;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli
index 1c96577a7..fd101414d 100644
--- a/helm/software/components/ng_refiner/nCicMetaSubst.mli
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli
@@ -67,9 +67,5 @@ 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
-
-val is_flexible : NCic.context -> subst:NCic.substitution -> NCic.term -> bool