Defs in context may now have an optional type (when unknown).

[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..a35c8d6c79d6fada2be3937a4566cbdf0e0418f7 100644 (file)
--- 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 :