Beta-expansion was avoided as soon as one argument was flexible.

[helm.git] / helm / software / components / ng_refiner / nCicMetaSubst.mli

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli
index 7bde2c1d6b2c7ea95e1a54ebd0c2d83880bae59f..92cfa0908311a30f4a4fbf5fc20779d26e480af7 100644 (file)
--- 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