X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Fcic_omdoc%2FdoubleTypeInference.ml;h=b514319c1f42bee7b8883b604f31cae8d02666ee;hb=28ac70d3f475442cda4ef30e0e9c0e6d012b2527;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..b514319c1 100644
--- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml
+++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
@@ -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