X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_acic%2FdoubleTypeInference.mli;h=dcc7b66bd19f6e6821b6651b2e527f9b55cab1a7;hb=aa791b78493b604792383cf6326877d0d53e0458;hp=892e09f8ac4d1172f96f4f1a8c42cbb265fca5f6;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/cic_acic/doubleTypeInference.mli b/components/cic_acic/doubleTypeInference.mli
index 892e09f8a..dcc7b66bd 100644
--- a/components/cic_acic/doubleTypeInference.mli
+++ b/components/cic_acic/doubleTypeInference.mli
@@ -6,14 +6,10 @@ 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
-val number_new_type_of_aux'_prop: int ref
-
 type types = {synthesized : Cic.term ; expected : Cic.term option};;
 
+val pack_coercion : (Cic.metasenv -> Cic.context -> Cic.term -> Cic.term) ref;;
+
 val double_type_of :
  Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option ->
   types Cic.CicHash.t