]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_acic/cic2acic.ml
Module CicHash (hash-tables over CIC terms based on physical equality) moved
[helm.git] / helm / ocaml / cic_acic / cic2acic.ml
index 1cdabc09fe673dd8ca222b5e376772612318e255..1943616226aa19005b0031cf4f86a8c649b72b8f 100644 (file)
@@ -118,7 +118,7 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
     if global_computeinnertypes then
      D.double_type_of metasenv context t expectedty
     else
-     D.CicHash.empty ()
+     Cic.CicHash.create 1 (* empty table *)
    in
 (*
    let time2 = Sys.time () in
@@ -157,7 +157,7 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
 (* *)
         let {D.synthesized = synthesized; D.expected = expected} =
          if computeinnertypes then
-          D.CicHash.find terms_to_types tt
+          Cic.CicHash.find terms_to_types tt
          else
           (* We are already in an inner-type and Coscoy's double *)
           (* type inference algorithm has not been applied.      *)