X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Funiverse.mli;h=9201d92b82ae5140b08ba701420b640525ca7716;hb=5649890273cf8e660bba744e84ce5fee1e5efe69;hp=ee5dc489aa63d9d1a1104032e2109527c8c5894c;hpb=b2a190e3c2d5b594d409db937e88f9f4f7d22b8c;p=helm.git

diff --git a/helm/software/components/tactics/universe.mli b/helm/software/components/tactics/universe.mli
index ee5dc489a..9201d92b8 100644
--- a/helm/software/components/tactics/universe.mli
+++ b/helm/software/components/tactics/universe.mli
@@ -37,6 +37,7 @@ val index_term_and_unfolded_term:
   universe -> Cic.context -> Cic.term -> Cic.term -> universe
 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: