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

diff --git a/helm/software/components/tactics/universe.mli b/helm/software/components/tactics/universe.mli
index ee5dc489a..5f9d612b5 100644
--- a/helm/software/components/tactics/universe.mli
+++ b/helm/software/components/tactics/universe.mli
@@ -24,19 +24,40 @@
  *)
 
 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
-val index:
-  universe -> 
-  Cic.term -> (* key *)
-  Cic.term -> (* value *)
-  universe
+
+(* index [univ] [key] [term] *)
+val index: universe -> Cic.term -> Cic.term -> universe
+
+(* collapse non-indexable terms, removing coercions an unfolding the head
+ * constant if any *)
 val keys: Cic.context -> Cic.term -> Cic.term list
-val key: Cic.term -> Cic.term
+
+(* 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
+
+(* indexex the term without coercions, with coercions and unfolded without
+ * coercions *)
 val index_local_term: 
   universe -> Cic.context -> Cic.term -> Cic.term -> universe
+
+(* pairs are (term,ty) *)
 val index_list: 
     universe -> Cic.context -> (Cic.term*Cic.term) list -> universe
 val remove: