X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fmetadata%2FmetadataExtractor.ml;h=63db2331d1f567e8b07306bda9744404961a78fc;hb=8dbc4dcef7328f3ac84f847255e9be8d47c1de6d;hp=4fbae1ba76ed43238afdc7cfb51b1d0fd329bf65;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/metadata/metadataExtractor.ml b/helm/software/components/metadata/metadataExtractor.ml
index 4fbae1ba7..63db2331d 100644
--- a/helm/software/components/metadata/metadataExtractor.ml
+++ b/helm/software/components/metadata/metadataExtractor.ml
@@ -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
 
@@ -119,7 +119,7 @@ let compute_term pos term =
         (*assert (not (is_main_pos pos));*)
         let set = aux (next_pos pos) set source in
         aux (next_pos pos) set target
-    | Cic.LetIn (_, term, target) ->
+    | Cic.LetIn (_, term, _, target) ->
         if is_main_pos pos then
           aux pos set (CicSubstitution.subst term target)
         else
@@ -210,7 +210,7 @@ let compute_metas term =
     | Cic.Lambda (_, source, target) ->
         let acc = aux in_hyp acc source in
         aux in_hyp acc target
-    | Cic.LetIn (_, term, target) ->
+    | Cic.LetIn (_, term, _, target) ->
         aux in_hyp acc (CicSubstitution.subst term target)
     | Cic.Appl [] -> assert false
     | Cic.Appl (hd :: tl) ->
@@ -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, _) ->