X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMkImplicit.mli;h=4f6fcee2e5d917ab06893638597e9e2b150f9839;hb=e6b28085c97ae7b9bd3f3262b105f6b84f42b047;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..4f6fcee2e 100644
--- a/helm/ocaml/cic_unification/cicMkImplicit.mli
+++ b/helm/ocaml/cic_unification/cicMkImplicit.mli
@@ -62,3 +62,5 @@ 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