From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 11 Oct 2007 08:44:09 +0000 (+0000)
Subject: Old inversion bug fixed: it used to work only on the last hypothesis (or sort
X-Git-Tag: make_still_working~5990
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0ca6c1688d9000997977e6b1bad9a8c997c81d08;p=helm.git

Old inversion bug fixed: it used to work only on the last hypothesis (or sort
of).
---

diff --git a/helm/software/components/tactics/inversion.ml b/helm/software/components/tactics/inversion.ml
index 19d0c739a..e61021244 100644
--- a/helm/software/components/tactics/inversion.ml
+++ b/helm/software/components/tactics/inversion.ml
@@ -336,8 +336,8 @@ 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