compose tactic restore and added nocomposites keyword

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

diff --git a/components/tactics/universe.mli b/components/tactics/universe.mli
index 4ae0ff961e2fa511c4ea8db2632629094fdcc4ce..ee5dc489aa63d9d1a1104032e2109527c8c5894c 100644 (file)
--- a/components/tactics/universe.mli
+++ b/components/tactics/universe.mli
@@ -32,6 +32,7 @@ val index:
   Cic.term -> (* value *)
   universe
 val keys: Cic.context -> Cic.term -> Cic.term list
+val key: Cic.term -> Cic.term
 val index_term_and_unfolded_term: 
   universe -> Cic.context -> Cic.term -> Cic.term -> universe
 val index_local_term: