Assert added to check whether an unsharing problem is met!

diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
index 7f09da68918ed5b886cfc2532abf405371db55dc..b514319c1f42bee7b8883b604f31cae8d02666ee 100644 (file)
--- 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