From 0b866fc2d78f8fa9a78b4d4c27e549379a79576f Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 2 Sep 2005 12:08:58 +0000
Subject: [PATCH] Assert added to check whether an unsharing problem is met!

---
 helm/ocaml/cic_omdoc/doubleTypeInference.ml | 1 +
 1 file changed, 1 insertion(+)

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