first moogle template checkin

[helm.git] / helm / ocaml / cic_omdoc / doubleTypeInference.mli

diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.mli b/helm/ocaml/cic_omdoc/doubleTypeInference.mli
index d7d06ae42346f96eb3cb89ab0128597b7d0e4d5e..20230e3bb0529ca2a36a0eb4ab94df8aa7d4cfe7 100644 (file)
--- a/helm/ocaml/cic_omdoc/doubleTypeInference.mli
+++ b/helm/ocaml/cic_omdoc/doubleTypeInference.mli
@@ -6,6 +6,12 @@ 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};;
 
 module CicHash :