X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Funiverse.mli;h=d74895114386bced7803090144fbbe7c96312607;hb=75620ca64e3038fcbebb51559fdc31b2e8a00f93;hp=de7c2087174b4be352a1b4dc838521c167a70af4;hpb=d030f02fa8a708cd663ffd0c5783770906b9b21a;p=helm.git

diff --git a/helm/software/components/tactics/universe.mli b/helm/software/components/tactics/universe.mli
index de7c20871..d74895114 100644
--- a/helm/software/components/tactics/universe.mli
+++ b/helm/software/components/tactics/universe.mli
@@ -40,6 +40,8 @@ val keys: Cic.context -> Cic.term -> Cic.term list
 (* 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