X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_acic%2FdoubleTypeInference.ml;h=98d12ceca9446e7c6550e1625d2938c38d22d60b;hb=9d4a3a25b327bb2c15bd0cff116ba6698b1a4335;hp=69287243918419218848f810371f5c0c1843fa83;hpb=9a0e4f3be9f70662f18d2d3b6dd60ae79fba565b;p=helm.git

diff --git a/helm/ocaml/cic_acic/doubleTypeInference.ml b/helm/ocaml/cic_acic/doubleTypeInference.ml
index 692872439..98d12ceca 100644
--- a/helm/ocaml/cic_acic/doubleTypeInference.ml
+++ b/helm/ocaml/cic_acic/doubleTypeInference.ml
@@ -114,7 +114,7 @@ let rec beta_reduce =
        let exp_named_subst' =
         List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
        in
-        C.Var (uri,exp_named_subst)
+        C.Var (uri,exp_named_subst')
     | C.Meta (n,l) ->
        C.Meta (n,
         List.map
@@ -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
 ;;