- Procedural: generation of "exact" is now complete

[helm.git] / helm / software / components / tactics / inversion.ml

diff --git a/helm/software/components/tactics/inversion.ml b/helm/software/components/tactics/inversion.ml
index 19d0c739ae87816ac9c26f6fded33d04f681ab37..3b4000ea4fb6fa1da810db0d300da3455a401ff3 100644 (file)
--- 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,_) ->
@@ -336,13 +336,13 @@ let inversion_tac ~term =
    for n = 1 to arity_consno do
     a := (Cic.Implicit None)::(!a)
    done;
-  (* apply    i_inv             ? ...?      H).     *)
-  Cic.Appl ([Cic.Const(uri,[])] @ !a @ [Cic.Rel 1])
+   (* apply    i_inv             ? ...?      H).     *)
+   Cic.Appl ([Cic.Const(uri,[])] @ !a @ [term])
   in
   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 =