X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2FdoubleTypeInference.ml;h=69287243918419218848f810371f5c0c1843fa83;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=7f09da68918ed5b886cfc2532abf405371db55dc;hpb=33cb5e3b6c50933f3af870ab66616e034638719d;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
index 7f09da689..692872439 100644
--- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml
+++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
@@ -324,12 +324,17 @@ let type_of_mutual_inductive_constr uri i j =
 ;;
 
 module CicHash =
- Hashtbl.Make
-  (struct
-    type t = Cic.term
-    let equal = (==)
-    let hash = Hashtbl.hash
-   end)
+  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 *)
@@ -635,6 +640,7 @@ 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 ;
       res