removed no longer used METAs

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

diff --git a/helm/ocaml/cic_acic/doubleTypeInference.mli b/helm/ocaml/cic_acic/doubleTypeInference.mli
index 138aad83440bcb062b00e637ca8a93bbfdf3898e..892e09f8ac4d1172f96f4f1a8c42cbb265fca5f6 100644 (file)
--- a/helm/ocaml/cic_acic/doubleTypeInference.mli
+++ b/helm/ocaml/cic_acic/doubleTypeInference.mli
@@ -14,16 +14,9 @@ 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
-;;
-
 val double_type_of :
- Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option -> types CicHash.t
+ Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option ->
+  types Cic.CicHash.t
 
 (** Auxiliary functions **)