in eta_finxing: type_of_aux' not called on eta_fixed terms

[helm.git] / helm / software / components / cic_acic / doubleTypeInference.mli

diff --git a/helm/software/components/cic_acic/doubleTypeInference.mli b/helm/software/components/cic_acic/doubleTypeInference.mli
index 86d8b23fabee6cac29723f5866a29dfb1f981d72..dcc7b66bd19f6e6821b6651b2e527f9b55cab1a7 100644 (file)
--- a/helm/software/components/cic_acic/doubleTypeInference.mli
+++ b/helm/software/components/cic_acic/doubleTypeInference.mli
@@ -6,12 +6,6 @@ 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;;