From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 30 Jun 2007 12:16:20 +0000 (+0000)
Subject: BU Conversion was not generated for Rels fixed. I wonder why...
X-Git-Tag: make_still_working~6230
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=29ff024ae2dca40fa476a2b8ffa1f16b1abf8288;p=helm.git

BU Conversion was not generated for Rels fixed. I wonder why...
---

diff --git a/helm/software/components/acic_content/acic2content.ml b/helm/software/components/acic_content/acic2content.ml
index 99bab2de4..f27b881ba 100644
--- a/helm/software/components/acic_content/acic2content.ml
+++ b/helm/software/components/acic_content/acic2content.ml
@@ -118,7 +118,11 @@ let test_for_lifting ~ids_to_inner_types ~ids_to_inner_sorts=
   let module C2A = Cic2acic in
   (* atomic terms are never lifted, according to my policy *)
   function
-      C.ARel (id,_,_,_) -> false
+      C.ARel (id,_,_,_) ->
+         (try 
+            ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
+            true;
+          with Not_found -> false) 
     | C.AVar (id,_,_) -> 
          (try 
             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;