]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_omdoc/doubleTypeInference.mli
A few modifications, here and there...
[helm.git] / helm / ocaml / cic_omdoc / doubleTypeInference.mli
index a35c8d6c79d6fada2be3937a4566cbdf0e0418f7..20230e3bb0529ca2a36a0eb4ab94df8aa7d4cfe7 100644 (file)
@@ -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