X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMkImplicit.mli;h=476270144c9de7cef4b1b3c8512b21ae4f47fcc0;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=7821bef400eb0c93f58dfb8ef17be9442907ba02;hpb=03dbf66cecebcfa5cf6b7ba8a9b0f0b0a55dde6e;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicMkImplicit.mli b/helm/ocaml/cic_unification/cicMkImplicit.mli
index 7821bef40..476270144 100644
--- a/helm/ocaml/cic_unification/cicMkImplicit.mli
+++ b/helm/ocaml/cic_unification/cicMkImplicit.mli
@@ -58,7 +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
-