X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.mli;h=92cfa0908311a30f4a4fbf5fc20779d26e480af7;hb=53bd7590de050214164c4f6b5181699dc38056f6;hp=7bde2c1d6b2c7ea95e1a54ebd0c2d83880bae59f;hpb=0f99c7691f8a418003acea3f7856102c21dcab8d;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli
index 7bde2c1d6..92cfa0908 100644
--- a/helm/software/components/ng_refiner/nCicMetaSubst.mli
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli
@@ -57,8 +57,6 @@ val saturate:
     NCic.context -> NCic.term -> int ->
        NCic.term * NCic.metasenv * NCic.term list
 
-val flexible: NCic.substitution -> NCic.term list -> bool
-
 val in_scope_tag : string
 val out_scope_tag : int -> string
 val is_out_scope_tag : string -> bool