Dead code removed.

[helm.git] / helm / ocaml / tactics / inversion.ml

diff --git a/helm/ocaml/tactics/inversion.ml b/helm/ocaml/tactics/inversion.ml
index 6b563fe6a0fae9451f2e7a5a0f2da9c85e54910e..5e442657d26c52578e7f32b67d5f1e79acb184d8 100644 (file)
--- 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