From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 2 Sep 2005 12:08:58 +0000 (+0000)
Subject: Assert added to check whether an unsharing problem is met!
X-Git-Tag: V_0_1_2_1~119
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0b866fc2d78f8fa9a78b4d4c27e549379a79576f;p=helm.git

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 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