]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_content/termAcicContent.ml
Added cprop <= type constraint.
[helm.git] / helm / software / components / acic_content / termAcicContent.ml
index f3806beea63896e2a3217df528a8806649328832..2ce47bb6761f1b953b2c078d994921bc7a3d9031 100644 (file)
@@ -42,7 +42,7 @@ type term_info =
   }
 
 let get_types uri =
-  let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+  let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
     match o with
       | Cic.InductiveDefinition (l,_,lpsno,_) -> l, lpsno 
       | _ -> assert false