]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_omdoc/doubleTypeInference.ml
Assert added to check whether an unsharing problem is met!
[helm.git] / helm / ocaml / cic_omdoc / doubleTypeInference.ml
index 7f09da68918ed5b886cfc2532abf405371db55dc..b514319c1f42bee7b8883b604f31cae8d02666ee 100644 (file)
@@ -635,6 +635,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