changed auto_tac params type and all derivate tactics like applyS and

[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 ee5dc489aa63d9d1a1104032e2109527c8c5894c..9201d92b82ae5140b08ba701420b640525ca7716 100644 (file)
--- 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: