X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicUntrusted.mli;h=7ff7f9335b6c2b5561171907fae35e12811ed73a;hb=a0b7db9844126ebcdf4b5dbb586514854cef5d93;hp=702f8fc19fe5d0f31f7738b2d31aaeb306e607b8;hpb=213cd54a013aca96640d611f2c6c65f7f8e24f4c;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicUntrusted.mli b/helm/software/components/ng_kernel/nCicUntrusted.mli index 702f8fc19..7ff7f9335 100644 --- a/helm/software/components/ng_kernel/nCicUntrusted.mli +++ b/helm/software/components/ng_kernel/nCicUntrusted.mli @@ -43,3 +43,5 @@ val apply_subst_metasenv : NCic.substitution -> NCic.metasenv -> NCic.metasenv val count_occurrences : subst:NCic.substitution -> int -> NCic.term -> int +(* quick, but with false negatives (since no ~subst), check for closed terms *) +val looks_closed : NCic.term -> bool