X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Finversion.ml;h=3b4000ea4fb6fa1da810db0d300da3455a401ff3;hb=281f0c7b4fc0d5b97025625af2ecff85edebbb5c;hp=e610212440ac9e71840859f2c76dccf14330f276;hpb=0ca6c1688d9000997977e6b1bad9a8c997c81d08;p=helm.git

diff --git a/helm/software/components/tactics/inversion.ml b/helm/software/components/tactics/inversion.ml
index e61021244..3b4000ea4 100644
--- a/helm/software/components/tactics/inversion.ml
+++ b/helm/software/components/tactics/inversion.ml
@@ -190,9 +190,9 @@ let private_inversion_tac ~term =
   | Some uri -> uri
  in
  let (_,context,goalty) = CicUtil.lookup_meta goal metasenv in
- let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+ let termty,_ = T.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
  let uri = baseuri_of_term termty in  
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
  let (_,_,typeno,_) =
   match termty with
    C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
@@ -215,7 +215,7 @@ let private_inversion_tac ~term =
  let parameters_tys =  
   (List.map 
    (fun t -> (
-    match (T.type_of_aux' metasenv context t CicUniv.empty_ugraph) with
+    match (T.type_of_aux' metasenv context t CicUniv.oblivion_ugraph) with
      (term,graph) -> term))
    parameters) 
  in
@@ -261,7 +261,7 @@ let private_inversion_tac ~term =
   (*DEBUG*) debug_print (lazy  ("private inversion: term before refinement: " ^ 
    CicPp.ppterm t));
  let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t 
-  CicUniv.empty_ugraph 
+  CicUniv.oblivion_ugraph 
  in
  (*DEBUG*) debug_print (lazy  ("private inversion: termine after refinement: "
   ^ CicPp.ppterm ref_t));
@@ -307,7 +307,7 @@ let inversion_tac ~term =
  (*DEBUG*) debug_print (lazy ("inversion begins"));
   let _,metasenv,_subst,_,_, _ = proof in
   let (_,context,goalty) = CicUtil.lookup_meta goal metasenv in
-  let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+  let termty,_ = T.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
   let uri, typeno = 
     match termty with
       | Cic.MutInd (uri,typeno,_) 
@@ -315,7 +315,7 @@ let inversion_tac ~term =
       | _ -> assert false
   in
   (* let uri = baseuri_of_term termty in *)
-  let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+  let obj,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
   let name,nleft,arity,cons_list =
    match obj with
     Cic.InductiveDefinition (tys,_,nleft,_) ->
@@ -342,7 +342,7 @@ let inversion_tac ~term =
   let t = appl_term (arity_length + (List.length cons_list)) inversor_uri in
   let (t1,metasenv,_subst,t3,t4, attrs) = proof in
   let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t
-  CicUniv.empty_ugraph 
+  CicUniv.oblivion_ugraph 
   in
   let proof = (t1,metasenv'',_subst,t3,t4, attrs) in
   let proof3,gl3 =