]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/metadata/metadataExtractor.ml
1) the home button of CicBrowser now works also for NG
[helm.git] / helm / software / components / metadata / metadataExtractor.ml
index 462679534c0488e1e4aa97a2255cb4b305fb34d4..63db2331d1f567e8b07306bda9744404961a78fc 100644 (file)
@@ -70,7 +70,7 @@ let incr_depth = function
   | _ -> assert false
 
 let var_has_body uri =
-  match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+  match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with
   | Cic.Variable (_, Some body, _, _, _), _ -> true
   | _ -> false
 
@@ -287,7 +287,7 @@ let depth_offset params =
   List.length (List.filter (non var_has_body) params)
 
 let rec compute_var pos 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.Variable (_, Some _, _, _, _) -> S.empty
     | Cic.Variable (_, None, ty, params, _) ->
@@ -310,7 +310,7 @@ let rec compute_var pos uri =
     | _ -> assert false 
 
 let compute_obj 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.Variable (_, body, ty, params, _)
   | Cic.Constant (_, body, ty, params, _) ->