X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Funiverse.mli;h=ee5dc489aa63d9d1a1104032e2109527c8c5894c;hb=34d2f477be65e3fd26bfb6d43a3dd0807274549b;hp=4ae0ff961e2fa511c4ea8db2632629094fdcc4ce;hpb=4fdd0bfa2337b0d35846cdfd63bd3c3bb6fbd3e5;p=helm.git

diff --git a/helm/software/components/tactics/universe.mli b/helm/software/components/tactics/universe.mli
index 4ae0ff961..ee5dc489a 100644
--- a/helm/software/components/tactics/universe.mli
+++ b/helm/software/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: