parameter sintax added to axiom statement

[helm.git] / helm / software / components / tactics / universe.mli

diff --git a/helm/software/components/tactics/universe.mli b/helm/software/components/tactics/universe.mli
index de7c2087174b4be352a1b4dc838521c167a70af4..5f9d612b5e97720705c16d122c2b01d1c027b7da 100644 (file)
--- 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
 
@@ -40,6 +46,8 @@ val keys: Cic.context -> Cic.term -> Cic.term list
 (* collapse non-indexable terms, not removing coercions *)
 val key: Cic.term -> Cic.term 
 
+val in_universe: universe -> Cic.term -> Cic.term option
+
 (* indexes the term and its unfolded both without coercions *)
 val index_term_and_unfolded_term: 
   universe -> Cic.context -> Cic.term -> Cic.term -> universe