X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Funiverse.mli;h=5f9d612b5e97720705c16d122c2b01d1c027b7da;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=d74895114386bced7803090144fbbe7c96312607;hpb=ec86d39f8d1c462a42d13b347f6e309b3d3936e7;p=helm.git

diff --git a/helm/software/components/tactics/universe.mli b/helm/software/components/tactics/universe.mli
index d74895114..5f9d612b5 100644
--- a/helm/software/components/tactics/universe.mli
+++ b/helm/software/components/tactics/universe.mli
@@ -27,6 +27,12 @@ type universe
 
 val empty : universe
 
+
+val iter : 
+  universe ->
+  (UriManager.uri Discrimination_tree.path -> Cic.term list -> unit) ->
+  unit
+
 (* retrieves the list of term that hopefully unify *)
 val get_candidates: universe -> Cic.term -> Cic.term list