X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Finversion.ml;h=5e442657d26c52578e7f32b67d5f1e79acb184d8;hb=06018c33636305c9b2b4f430091de2c3eb51e91a;hp=6b563fe6a0fae9451f2e7a5a0f2da9c85e54910e;hpb=da59a744767c799ad287489c55f2ff972f93d93c;p=helm.git

diff --git a/helm/ocaml/tactics/inversion.ml b/helm/ocaml/tactics/inversion.ml
index 6b563fe6a..5e442657d 100644
--- a/helm/ocaml/tactics/inversion.ml
+++ b/helm/ocaml/tactics/inversion.ml
@@ -165,7 +165,6 @@ let inversion_tac ~term =
  let inversion_tac ~term (proof, goal) =
  let (_,metasenv,_,_) = proof in
  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let (newproof, metasenv') = PEH.subst_meta_in_proof proof metano term [] in
  let uri_of_eq = HelmLibraryObjects.Logic.eq_URI in
 
  (* dall'indice che indentifica il goal nel metasenv, ritorna il suo tipo, che