]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/library/cicRecord.ml
removed debug pps
[helm.git] / helm / software / components / library / cicRecord.ml
index 775292ccbb4c959892707be7eaa33a5e8df68236..5502f989e9ca0149bdb4d39366cfda61edc95421 100644 (file)
@@ -43,7 +43,7 @@ let generate_one_proj uri params paramsno fields t i =
 
 let projections_of uri field_names =
  let buri = UriManager.buri_of_uri uri in
- let obj,ugraph = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in
+ let obj,ugraph = CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri in
   match obj with
      Cic.InductiveDefinition ([_,_,sort,[_,ty]],params,paramsno,_) ->
       assert (params = []); (* general case not implemented *)