X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicUntrusted.mli;h=bb5aa304974cbebe30fcd993e7d9adb91af1fab8;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=7ff7f9335b6c2b5561171907fae35e12811ed73a;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicUntrusted.mli b/helm/software/components/ng_kernel/nCicUntrusted.mli
index 7ff7f9335..bb5aa3049 100644
--- a/helm/software/components/ng_kernel/nCicUntrusted.mli
+++ b/helm/software/components/ng_kernel/nCicUntrusted.mli
@@ -19,7 +19,6 @@ val map_obj_kind:
   ?skip_body:bool -> (NCic.term -> NCic.term) -> NCic.obj_kind -> NCic.obj_kind
 
 val metas_of_term : NCic.substitution -> NCic.context -> NCic.term -> int list
-val sort_metasenv: NCic.substitution -> NCic.metasenv -> NCic.metasenv
 
 type meta_kind = [ `IsSort | `IsType | `IsTerm ]
 val kind_of_meta: NCic.meta_attrs -> meta_kind
@@ -40,8 +39,3 @@ val apply_subst : NCic.substitution -> NCic.context -> NCic.term -> NCic.term
 val apply_subst_context : fix_projections:bool -> 
   NCic.substitution -> NCic.context -> NCic.context
 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