X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_acic%2FdoubleTypeInference.ml;h=b28359bd7857a9ebf0b36e092ba7ca9991b4c47b;hb=86241d46558e3a4979fc786e47ce78f90eb9190c;hp=69287243918419218848f810371f5c0c1843fa83;hpb=20a35144a63d112d7eedc092ccd3366473021ef9;p=helm.git

diff --git a/helm/ocaml/cic_acic/doubleTypeInference.ml b/helm/ocaml/cic_acic/doubleTypeInference.ml
index 692872439..b28359bd7 100644
--- a/helm/ocaml/cic_acic/doubleTypeInference.ml
+++ b/helm/ocaml/cic_acic/doubleTypeInference.ml
@@ -323,20 +323,6 @@ let type_of_mutual_inductive_constr uri i j =
     | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
 ;;
 
-module CicHash =
-  struct
-    module Tmp = 
-     Hashtbl.Make
-      (struct
-        type t = Cic.term
-        let equal = (==)
-        let hash = Hashtbl.hash
-       end)
-    include Tmp
-    let empty () = Tmp.create 1
-  end
-;;
-
 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
 let rec type_of_aux' subterms_to_types metasenv context t expectedty =
  (* Coscoy's double type-inference algorithm             *)
@@ -640,8 +626,8 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
           {synthesized = synthesized' ; expected = Some expectedty'},
           expectedty'
      in
-      assert (not (CicHash.mem subterms_to_types t));
-      CicHash.add subterms_to_types t types ;
+      assert (not (Cic.CicHash.mem subterms_to_types t));
+      Cic.CicHash.add subterms_to_types t types ;
       res
 
  and visit_exp_named_subst context uri exp_named_subst =
@@ -746,7 +732,7 @@ and type_of_branch context argsno need_dummy outtype term constype =
 ;;
 
 let double_type_of metasenv context t expectedty =
- let subterms_to_types = CicHash.create 503 in
+ let subterms_to_types = Cic.CicHash.create 503 in
   ignore (type_of_aux' subterms_to_types metasenv context t expectedty) ;
   subterms_to_types
 ;;