ocaml 3.09 transition

[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..138aad83440bcb062b00e637ca8a93bbfdf3898e 100644 (file)
--- a/helm/ocaml/cic_omdoc/doubleTypeInference.mli
+++ b/helm/ocaml/cic_omdoc/doubleTypeInference.mli
@@ -6,12 +6,19 @@ 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 :
   sig
     type 'a t
     val find : 'a t -> Cic.term -> 'a
+    val empty: unit -> 'a t
   end
 ;;