X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2FdoubleTypeInference.mli;h=138aad83440bcb062b00e637ca8a93bbfdf3898e;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=a35c8d6c79d6fada2be3937a4566cbdf0e0418f7;hpb=c706b1cb2c7cbdd23a3281d35d3f0b10c3a684cf;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.mli b/helm/ocaml/cic_omdoc/doubleTypeInference.mli
index a35c8d6c7..138aad834 100644
--- a/helm/ocaml/cic_omdoc/doubleTypeInference.mli
+++ b/helm/ocaml/cic_omdoc/doubleTypeInference.mli
@@ -6,6 +6,7 @@ exception WrongUriToMutualInductiveDefinitions of string
 exception ListTooShort
 exception RelToHiddenHypothesis
 
+val syntactic_equality_add_time: float ref
 val type_of_aux'_add_time: float ref
 val number_new_type_of_aux'_double_work: int ref
 val number_new_type_of_aux': int ref
@@ -17,6 +18,7 @@ module CicHash :
   sig
     type 'a t
     val find : 'a t -> Cic.term -> 'a
+    val empty: unit -> 'a t
   end
 ;;