X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMkImplicit.mli;fp=helm%2Focaml%2Fcic_unification%2FcicMkImplicit.mli;h=476270144c9de7cef4b1b3c8512b21ae4f47fcc0;hb=8523a35427aa3fdf40a0e14b8aac3428c8aa13f0;hp=4f6fcee2e5d917ab06893638597e9e2b150f9839;hpb=dbe5d5ee749b3d5d36c91f96b73d7554967fc8cd;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicMkImplicit.mli b/helm/ocaml/cic_unification/cicMkImplicit.mli
index 4f6fcee2e..476270144 100644
--- a/helm/ocaml/cic_unification/cicMkImplicit.mli
+++ b/helm/ocaml/cic_unification/cicMkImplicit.mli
@@ -58,9 +58,3 @@ val fresh_subst:
         UriManager.uri list -> 
           Cic.metasenv * (Cic.term Cic.explicit_named_substitution)
 
-val expand_implicits:
-  Cic.metasenv -> Cic.substitution -> Cic.context -> Cic.term ->
-    Cic.metasenv * Cic.term
-
-val expand_implicits_in_obj:
-  Cic.metasenv -> Cic.substitution -> Cic.obj -> Cic.metasenv * Cic.obj