]> matita.cs.unibo.it Git - helm.git/commitdiff
BU Conversion was not generated for Rels fixed. I wonder why...
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 30 Jun 2007 12:16:20 +0000 (12:16 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 30 Jun 2007 12:16:20 +0000 (12:16 +0000)
helm/software/components/acic_content/acic2content.ml

index 99bab2de44f122fc7d099ba331982bdbe7304409..f27b881ba888a68653bb2393f6168d03084f6f8f 100644 (file)
@@ -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;