X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2FdoubleTypeInference.mli;h=a35c8d6c79d6fada2be3937a4566cbdf0e0418f7;hb=f480a8792f70b765c5e15cc16f1251ac6bc21d01;hp=d7d06ae42346f96eb3cb89ab0128597b7d0e4d5e;hpb=4bcd14a9ed245ccae631697a05ff5a377c02b179;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.mli b/helm/ocaml/cic_omdoc/doubleTypeInference.mli
index d7d06ae42..a35c8d6c7 100644
--- a/helm/ocaml/cic_omdoc/doubleTypeInference.mli
+++ b/helm/ocaml/cic_omdoc/doubleTypeInference.mli
@@ -6,6 +6,11 @@ exception WrongUriToMutualInductiveDefinitions of string
 exception ListTooShort
 exception RelToHiddenHypothesis
 
+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
+val number_new_type_of_aux'_prop: int ref
+
 type types = {synthesized : Cic.term ; expected : Cic.term option};;
 
 module CicHash :