X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FdoubleTypeInference.mli;h=d7d06ae42346f96eb3cb89ab0128597b7d0e4d5e;hb=bd1567199bf9a875cd3cef3b0301d359ad008867;hp=4de5bc00c16c19523861917a63f36c1d26a1d2a6;hpb=cedc0cfe0ea81f94ac8b88b71d8f855a33329593;p=helm.git

diff --git a/helm/gTopLevel/doubleTypeInference.mli b/helm/gTopLevel/doubleTypeInference.mli
index 4de5bc00c..d7d06ae42 100644
--- a/helm/gTopLevel/doubleTypeInference.mli
+++ b/helm/gTopLevel/doubleTypeInference.mli
@@ -6,14 +6,20 @@ exception WrongUriToMutualInductiveDefinitions of string
 exception ListTooShort
 exception RelToHiddenHypothesis
 
-type types = {synthesized : Cic.term ; expected : Cic.term};;
+type types = {synthesized : Cic.term ; expected : Cic.term option};;
 
 module CicHash :
   sig
-    type key = Cic.term
-    and 'a t
-    val find : 'a t -> key -> 'a
+    type 'a t
+    val find : 'a t -> Cic.term -> 'a
   end
+;;
 
 val double_type_of :
- Cic.metasenv -> Cic.context -> Cic.term -> types CicHash.t
+ Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option -> types CicHash.t
+
+(** Auxiliary functions **)
+
+(* does_not_occur n te                              *)
+(* returns [true] if [Rel n] does not occur in [te] *)
+val does_not_occur : int -> Cic.term -> bool